OAI/Analysis/LipschitzHilbert/Trees/SourceLongCellMask.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual parent-witness density test supplies the common mask and mass bounds on the disjoint cells used in long-tree integration.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_long_cell_mask line 18
  2. abbrev OAI.LipschitzHilbert.SourceLabeledLattice.DensityWhitneyCell line 60
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.HasLongPacket line 63
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.long_cell_scale_le_top line 66
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_whitney_masks line 75

    Source documentation

    Choose the density masks on the entire actual Whitney partition. Cells without long packets receive the empty mask.

    theorem exists_whitney_masks
    (b : ℝ) (cell : ∀ j, P.labels j → ℤ) (grid : ℤ) (tau : ℝ)
    (htime : P.topLength≤tau)
    (hY : ∀ a : P.PacketIndex, |P.actualZ a.1 a.2.1 a.2.2-b|≤P.width/2)
    (hreference : ∀ a : P.PacketIndex, 0∈
      scaledAngularCell (P.width/P.topLength) grid a.1.val (cell a.1 a.2.1))
    (E : Set (ℝ×ℝ)) (hE : MeasurableSet E) (u : ℝ×ℝ → ℝ) (hu : Measurable u)
    (eta : ℝ) (heta : 0≤eta)
    (hdensity : ∀ a, P.ordinaryDensity 0 cell grid P.width tau E u a≤eta) :
    ∃ Omega : P.DensityWhitneyCell → Set ℝ,
      (∀ i, MeasurableSet (Omega i)) ∧
      (∀ i, ¬P.HasLongPacket i → Omega i=∅) ∧
…

    Mentions: OAI.LipschitzHilbert.scaledAngularCell