SourceWhitneyDensityTest.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual parent witness furnishes an admissible density test at a length between sixteen and thirty-two Whitney lengths.

theorem OAI.LipschitzHilbert.SourceWhitney.center_mem_cell line 12
theorem OAI.LipschitzHilbert.SourceWhitney.exists_comparable_test_length line 24
Source documentation
No compatibility of the horizontal grid origin with the packet length is assumed: the test length is selected in the source scale grid.
```
theorem exists_comparable_test_length (ell0 r : ℝ) (hell0 : 0<ell0) (hr : 0<r) :
    ∃ level : ℤ, 16*r≤ell0/scale level ∧ ell0/scale level<32*r := by
…
```

theorem OAI.LipschitzHilbert.SourceWhitney.exists_whitney_density_test line 39

Source documentation

A Whitney interval admitting a tile longer than thirty-two interval lengths has an actual density test containing its parent witness.

theorem exists_whitney_density_test {ι : Type*} (tiles : Finset ι)
    (tile : ι → OrdinaryDensityTile) (ell0 w W tau slope y : ℝ) (grid k j : ℤ)
    (hell0 : 0<ell0) (hW : 0<W)
    (hWhitney : Whitney tiles (fun i => (tile i).center.1)
      (fun i => ell0/scale (tile i).level) k j)
    (hshort : ∀ i∈tiles, ell0/scale (tile i).level≤tau)
    (hcenter : ∀ i∈tiles, |(tile i).center.2-y-slope*(tile i).center.1|≤W/2)
    (hslope : ∀ i∈tiles, slope∈scaledAngularCell (w/ell0) grid (tile i).level (tile i).cell)
    (hlong : ∃ i∈tiles, 32*scale k<ell0/scale (tile i).level) :
    ∃ i∈tiles, ∃ test : OrdinaryDensityTest ell0 w W tau grid (tile i),
      test.top.x=center k j ∧ test.top.y=y+slope*center k j ∧
      test.top.slope=slope ∧ 16*scale k≤test.top.length ∧ test.top.length<32*scale k := by
…

Mentions: OAI.LipschitzHilbert.OrdinaryDensityTile, OAI.LipschitzHilbert.SourceWhitney.Whitney, OAI.LipschitzHilbert.scaledAngularCell, OAI.LipschitzHilbert.OrdinaryDensityTest, OAI.LipschitzHilbert.SourceWhitney.center

theorem OAI.LipschitzHilbert.SourceWhitney.exists_whitney_cell_density line 87

Source documentation

The test selected from the parent witness gives the manuscript's polynomial cell-density bound, simultaneously at every transverse index.

theorem exists_whitney_cell_density {ι : Type*} (tiles : Finset ι)
    (tile : ι → OrdinaryDensityTile) (ell0 w W tau slope y : ℝ) (grid k j : ℤ)
    (hell0 : 0<ell0) (hW : 0<W)
    (hWhitney : Whitney tiles (fun i => (tile i).center.1)
      (fun i => ell0/scale (tile i).level) k j)
    (hshort : ∀ i∈tiles, ell0/scale (tile i).level≤tau)
    (hcenter : ∀ i∈tiles, |(tile i).center.2-y-slope*(tile i).center.1|≤W/2)
    (hslope : ∀ i∈tiles, slope∈scaledAngularCell (w/ell0) grid (tile i).level (tile i).cell)
    (hlong : ∃ i∈tiles, 32*scale k<ell0/scale (tile i).level)
    (E : Set (ℝ×ℝ)) (hE : MeasurableSet E) (u : ℝ×ℝ → ℝ) (hu : Measurable u)
    (eta : ℝ) (heta : 0≤eta)
    (hdensity : ∀ i∈tiles, (tile i).density ell0 w W tau grid E u≤eta) :
…

Mentions: OAI.LipschitzHilbert.OrdinaryDensityTile, OAI.LipschitzHilbert.SourceWhitney.Whitney, OAI.LipschitzHilbert.scaledAngularCell