SourceTreeCellDensity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The density factor for a long-tree cell. A literal admissible test controls the measure of its angularly restricted cell, with polynomial loss in the transverse cell index.

theorem OAI.LipschitzHilbert.one_le_densityKernel_mul line 13

theorem OAI.LipschitzHilbert.density_test_cell_mass line 30

Source documentation

A density test gives the mass bound on any measurable cell on which its normalized radius is bounded. The constant function is integrable on the restricted cell as a consequence, without an extra finiteness premise.

theorem density_test_cell_mass (ell0 w W tau : ℝ) (grid : ℤ)
    (tile : OrdinaryDensityTile) (test : OrdinaryDensityTest ell0 w W tau grid tile)
    (E : Set (ℝ×ℝ)) (hE : MeasurableSet E) (u : ℝ×ℝ → ℝ) (hu : Measurable u)
    (S : Set (ℝ×ℝ)) (hS : MeasurableSet S) (R eta : ℝ) (hR : 0≤R)
    (hradius : ∀ z∈S, test.top.radius z≤R)
    (hdensity : tile.density ell0 w W tau grid E u≤eta) :
    let A := E∩u ⁻¹' scaledAngularCell (w/ell0) grid test.level test.cell∩S
…

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

def OAI.LipschitzHilbert.SourceWhitney.treeCell line 74
Source documentation
Horizontal Whitney strip crossed with one transverse cell in the reference coordinates of a tree.
```
def treeCell (slope y W : ℝ) (k j n : ℤ) : Set (ℝ×ℝ) :=
…
```
theorem OAI.LipschitzHilbert.SourceWhitney.treeCell_measurable line 77
theorem OAI.LipschitzHilbert.SourceWhitney.treeCell_radius_bound line 85
Source documentation
A test centered on the horizontal cell has bounded radius on each transverse translate.
```
theorem treeCell_radius_bound (T : SlopeBox) (slope y : ℝ) (k j n : ℤ)
    (hx : T.x=center k j) (hy : T.y=y+slope*T.x) (ht : T.slope=slope)
    (hlength : scale k≤T.length) {z : ℝ×ℝ} (hz : z∈treeCell slope y T.width k j n) :
    T.radius z≤1+|(n:ℝ)| := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceWhitney.center, OAI.LipschitzHilbert.SourceWhitney.treeCell