SourceWhitneyGluing.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Glue stripwise estimates over the actual countable Whitney partition. Finite-subfamily bounds imply integrability and the same global bound.

abbrev OAI.LipschitzHilbert.SourceWhitney.CellIndex line 16
theorem OAI.LipschitzHilbert.SourceWhitney.exists_cellIndex line 21
def OAI.LipschitzHilbert.SourceWhitney.indexAt line 27
Source documentation
The unique maximal allowed dyadic cell containing a given point.
```
def indexAt (z : ℝ) : CellIndex tiles x ell :=
…
```
Mentions: OAI.LipschitzHilbert.SourceWhitney.CellIndex
theorem OAI.LipschitzHilbert.SourceWhitney.indexAt_mem line 30
theorem OAI.LipschitzHilbert.SourceWhitney.indexAt_eq_of_mem line 34
def OAI.LipschitzHilbert.SourceWhitney.strip line 42
theorem OAI.LipschitzHilbert.SourceWhitney.strip_measurable line 45
theorem OAI.LipschitzHilbert.SourceWhitney.strip_disjoint line 49
theorem OAI.LipschitzHilbert.SourceWhitney.strip_iUnion line 58
def OAI.LipschitzHilbert.SourceWhitney.paste line 69
Source documentation
Evaluate the local function belonging to the unique Whitney strip.
```
def paste (F : CellIndex tiles x ell → ℝ×ℝ → V) (z : ℝ×ℝ) : V :=
…
```
Mentions: OAI.LipschitzHilbert.SourceWhitney.CellIndex
theorem OAI.LipschitzHilbert.SourceWhitney.paste_eq line 72

theorem OAI.LipschitzHilbert.SourceWhitney.paste_integrable_bound line 82

Source documentation

Uniform bounds for finite collections of local norm integrals give integrability and the identical estimate on the full Whitney partition.

theorem paste_integrable_bound (E : Set (ℝ×ℝ)) (hE : MeasurableSet E)
    (F : CellIndex tiles x ell → ℝ×ℝ → V)
    (hF : ∀ i, IntegrableOn (F i) (strip tiles x ell E i) (volume.prod volume))
    (C : ℝ) (hbound : ∀ S : Finset (CellIndex tiles x ell),
      (∑ i∈S, ∫ z in strip tiles x ell E i, ‖F i z‖ ∂volume.prod volume) ≤ C) :
    IntegrableOn (paste tiles x ell hne hpos F) E (volume.prod volume) ∧
    (∫ z in E, ‖paste tiles x ell hne hpos F z‖ ∂volume.prod volume) ≤ C := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.CellIndex, OAI.LipschitzHilbert.SourceWhitney.strip, OAI.LipschitzHilbert.SourceWhitney.paste