OAI/Analysis/LipschitzHilbert/Trees/SourceTreeCellGluing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LipschitzHilbert.SourceWhitney.ProductCellIndex line 16
2. def OAI.LipschitzHilbert.SourceWhitney.productCell line 18
3. theorem OAI.LipschitzHilbert.SourceWhitney.productCell_measurable line 21
4. theorem OAI.LipschitzHilbert.SourceWhitney.productCell_disjoint line 24
5. theorem OAI.LipschitzHilbert.SourceWhitney.productCell_iUnion line 40
6. theorem OAI.LipschitzHilbert.SourceWhitney.product_finite_bound line 51

   Source documentation

   Any finite collection is dominated by its finite rectangle of horizontal and transverse indices.

   theorem product_finite_bound
       (F : ProductCellIndex tiles x ell → ℝ) (hF : ∀ i, 0≤F i) (C : ℝ)
       (hrect : ∀ (S : Finset (CellIndex tiles x ell)) (T : Finset ℤ),
         (∑ i∈S×ˢT, F i)≤C) (A : Finset (ProductCellIndex tiles x ell)) :
       (∑ i∈A, F i)≤C := by
   …

   Mentions: OAI.LipschitzHilbert.SourceWhitney.ProductCellIndex, OAI.LipschitzHilbert.SourceWhitney.CellIndex

7. theorem OAI.LipschitzHilbert.SourceWhitney.product_paste_integrable_bound line 66

   Source documentation

   Integrability of the pasted function follows from the proved local integrals and their uniform finite-rectangle bound.

   theorem product_paste_integrable_bound (b W : ℝ) (hW : 0<W)
       (F : CellIndex tiles x ell → ℝ×ℝ → V)
       (hF : ∀ i : ProductCellIndex tiles x ell,
         IntegrableOn (F i.1) (productCell tiles x ell b W i) (volume.prod volume))
       (C : ℝ) (hrect : ∀ (S : Finset (CellIndex tiles x ell)) (T : Finset ℤ),
         (∑ i∈S×ˢT, ∫ z in productCell tiles x ell b W i, ‖F i.1 z‖ ∂volume.prod volume)≤C) :
       Integrable (paste tiles x ell hne hpos F) (volume.prod volume) ∧
         (∫ z, ‖paste tiles x ell hne hpos F z‖ ∂volume.prod volume)≤C := by
   …

   Mentions: OAI.LipschitzHilbert.SourceWhitney.CellIndex, OAI.LipschitzHilbert.SourceWhitney.ProductCellIndex, OAI.LipschitzHilbert.SourceWhitney.productCell, OAI.LipschitzHilbert.SourceWhitney.paste