OAI/Analysis/LipschitzHilbert/Packets/SourcePacketLongCell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_whitney_cell_density line 17

   Source documentation

   The original long selectors all live in one angular cell whose mass on every transverse strip has the density bound from the manuscript.

   theorem source_whitney_cell_density (P : SourceLabeledLattice N κ Label Item)
       (oldSlope y : ℝ) (cell : ∀ j, P.labels j → ℤ) (grid k j : ℤ) (w tau : ℝ)
       (htime : P.topLength≤tau)
       (hWhitney : Whitney (Finset.univ : Finset P.PacketIndex)
         (fun q => P.actualX q.1 q.2.1 q.2.2) (fun q => P.length q.1) k j)
       (hY : ∀ q : P.PacketIndex, |P.actualZ q.1 q.2.1 q.2.2-y|≤P.width/2)
       (hreference : ∀ q : P.PacketIndex, oldSlope∈
         scaledAngularCell (w/P.topLength) grid q.1.val (cell q.1 q.2.1))
       (hlong : ∃ q : P.PacketIndex, 32*DyadicLineGrid.scale k<P.length q.1)
       (E : Set (ℝ×ℝ)) (hE : MeasurableSet E) (u : ℝ×ℝ → ℝ) (hu : Measurable u)
       (eta : ℝ) (heta : 0≤eta)
       (hdensity : ∀ q, P.ordinaryDensity oldSlope cell grid w tau E u q≤eta) :
   …

   Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.scaledAngularCell, OAI.LipschitzHilbert.DyadicLineGrid.scale