SourceLongTreeSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Original long-packet angular supports lie in the cell of the actual Whitney density test. This is the common indicator kept on the frozen main term and the selector error.

theorem OAI.LipschitzHilbert.OrdinaryDensityTest.contains_longer_angular_cell line 14

theorem OAI.LipschitzHilbert.long_selector_support line 29

Source documentation

Every long original selector vanishes outside the single test cell. The conclusion applies before any freezing or error decomposition.

theorem long_selector_support {ι κ : Type*} {ell0 w W tau : ℝ} {grid : ℤ}
    {witness : OrdinaryDensityTile} (test : OrdinaryDensityTest ell0 w W tau grid witness)
    (hell0 : 0<ell0) (tiles : Finset ι) (tile : ι → OrdinaryDensityTile)
    (selector : ι → κ → ℝ → ℂ)
    (hsupport : ∀ i∈tiles, ∀ a s, selector i a s≠0 →
      s∈scaledAngularCell (w/ell0) grid (tile i).level (tile i).cell)
    (hlen : ∀ i∈tiles, test.top.length≤ell0/DyadicLineGrid.scale (tile i).level)
    (hslope : ∀ i∈tiles, test.top.slope∈scaledAngularCell (w/ell0) grid (tile i).level (tile i).cell)
    {s : ℝ} (hs : s∉scaledAngularCell (w/ell0) grid test.level test.cell) :
    ∀ i∈tiles, ∀ a, selector i a s=0 := by
…

Mentions: OAI.LipschitzHilbert.OrdinaryDensityTile, OAI.LipschitzHilbert.OrdinaryDensityTest, OAI.LipschitzHilbert.scaledAngularCell, OAI.LipschitzHilbert.DyadicLineGrid.scale