OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceMasks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reference-direction masks obtained from the original angular grid. Only the direction variable is translated; no dyadic cell is reassigned.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_reference_long_cell_mask line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_reference_whitney_masks line 73

    Source documentation

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

    theorem exists_reference_whitney_masks
    (t b w : ℝ) (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, t∈
      scaledAngularCell (w/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 t cell grid w tau E u a≤eta) :
    ∃ Omega : P.DensityWhitneyCell → Set ℝ,
      (∀ i, MeasurableSet (Omega i)) ∧
      (∀ i, ¬P.HasLongPacket i → Omega i=∅) ∧
…

    Mentions: OAI.LipschitzHilbert.scaledAngularCell