Theorems · Inductive type · real analysis

BoxIntegral.IntegrationParams.MemBaseSet

{ι : Type u_1} →
  [Fintype ι] →
    BoxIntegral.IntegrationParams →
      (I : BoxIntegral.Box ι) → NNReal → ((ι → ℝ) → ↑(Set.Ioi 0)) → BoxIntegral.TaggedPrepartition I → Prop

The predicate corresponding to a base set of the filter defined by an IntegrationParams. It says that * if l.bHenstock, then π is a Henstock prepartition, i.e. each tag belongs to the corresponding closed box; * π is subordinate to r; * if l.bDistortion, then the distortion of each box in π is less than or equal to c; * if l.bDistortion, then there exists a prepartition π' with distortion ≤ c that covers exactly I \ π.iUnion. The last condition is automatically verified for partitions, and is used in the proof of the Sacks-Henstock inequality to compare two prepartitions covering the same part of the box. It is also automatically satisfied for any c > 1, see TODO section of the module docstring for details.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Filter

Cited by

34 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype