OAI/Analysis/LipschitzHilbert/Trees/SourceDensityRebase.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.OrdinaryDensityTile.rebase line 13
2. theorem OAI.LipschitzHilbert.density_rebase_length line 16
3. theorem OAI.LipschitzHilbert.density_rebase_cell line 21
4. def OAI.LipschitzHilbert.OrdinaryDensityTest.rebase line 30
5. theorem OAI.LipschitzHilbert.density_rebase_test_value line 49

   Source documentation

   Each original test has exactly the same weighted average after rebasing.

   theorem density_rebase_test_value {ell0 w W tau : ℝ} {q : ℤ} {tile : OrdinaryDensityTile}
       (test : OrdinaryDensityTest ell0 w W tau q tile)
       (h : ℤ) (hell0 : 0<ell0) (hw : 0<w)
       (E : Set (ℝ×ℝ)) (u : ℝ×ℝ → ℝ) :
       densityAverage (test.rebase h hell0 hw).top E u
         (scaledAngularCell (w/(ell0/scale h)) ((h.negOnePow : ℤ)*q)
           (test.rebase h hell0 hw).level (test.rebase h hell0 hw).cell)=
       densityAverage test.top E u (scaledAngularCell (w/ell0) q test.level test.cell) := by
   …

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

6. def OAI.LipschitzHilbert.OrdinaryDensityTest.restore line 59
7. theorem OAI.LipschitzHilbert.density_restore_test_value line 82
8. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.density_rebase line 96

   Source documentation

   All weighted box tests, including tests above the initial scale, correspond in both directions, hence the density is exactly preserved.

   theorem OrdinaryDensityTile.density_rebase (tile : OrdinaryDensityTile)
       (ell0 w W tau : ℝ) (h : ℤ) (q : ℤ) (hell0 : 0<ell0) (hw : 0<w)
       (E : Set (ℝ×ℝ)) (u : ℝ×ℝ → ℝ) :
       (tile.rebase h).density (ell0/scale h) w W tau ((h.negOnePow : ℤ)*q) E u=
         tile.density ell0 w W tau q E u := by
   …

   Mentions: OAI.LipschitzHilbert.OrdinaryDensityTile, OAI.LipschitzHilbert.OrdinaryDensityTile.density