SourceAngularLongCellMask.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The same parent-witness density masks at an independent angular width. Spatial strip volumes remain determined by P.width.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_angular_long_cell_mask line 16

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_angular_whitney_masks line 53

Source documentation

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

theorem exists_angular_whitney_masks
    (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, 0∈
      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 0 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