OAI/Analysis/LipschitzHilbert/Phase/AngularGrid.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LipschitzHilbert.AngularGrid line 16

   Source documentation

   A single common translation is used at every angular level.

   structure AngularGrid where
   …

2. def OAI.LipschitzHilbert.AngularGrid.index line 25
3. def OAI.LipschitzHilbert.AngularGrid.eligible line 28
4. theorem OAI.LipschitzHilbert.AngularGrid.index_parent line 31
5. theorem OAI.LipschitzHilbert.AngularGrid.eligible_parent line 38
6. def OAI.LipschitzHilbert.AngularGrid.cellTops line 55

   Source documentation

   The tops in an actual translated angular cell, with the scale cutoff included in membership rather than imposed after assigning the cell.

   def cellTops (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
       (cutoff : ℝ) (level : ℕ) (cell : ℤ) : Finset ι := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

7. theorem OAI.LipschitzHilbert.AngularGrid.mem_cellTops line 60
8. theorem OAI.LipschitzHilbert.AngularGrid.cellTops_subset_parent line 67
9. def OAI.LipschitzHilbert.AngularGrid.mass line 78
10. theorem OAI.LipschitzHilbert.AngularGrid.mass_nonnegative line 82
11. theorem OAI.LipschitzHilbert.AngularGrid.mass_pos_of_member line 88
12. theorem OAI.LipschitzHilbert.AngularGrid.path_mass_pos line 97

    Source documentation

    An eligible top supplies a strictly positive summand on its own path.

    theorem path_mass_pos (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
        (cutoff : ℝ) (weight : ι → X → ℝ) (hw : ∀ i x, 0 < weight i x)
        (level : ℕ) (top : ι) (htop : top ∈ tops) (heligible : g.eligible cutoff (precision top) level)
        (x : X) : 0 < g.mass tops slope precision cutoff weight level (g.index level (slope top)) x :=
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

13. theorem OAI.LipschitzHilbert.AngularGrid.mass_le_total line 105

    Source documentation

    Every angular mass is a submass of the fixed total top weight.

    theorem mass_le_total (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
        (cutoff : ℝ) (weight : ι → X → ℝ) (hw : ∀ i x, 0 ≤ weight i x)
        (level : ℕ) (cell : ℤ) (x : X) :
        g.mass tops slope precision cutoff weight level cell x ≤ ∑ i ∈ tops, weight i x := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

14. theorem OAI.LipschitzHilbert.AngularGrid.mass_le_parent line 117

    Source documentation

    Child mass is at most parent mass, with the eligibility restriction already built into both finite sums.

    theorem mass_le_parent (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
        (cutoff : ℝ) (weight : ι → X → ℝ) (hp : ∀ i ∈ tops, 0 ≤ precision i)
        (hw : ∀ i x, 0 ≤ weight i x) (level : ℕ) (child : ℤ) (x : X) :
        g.mass tops slope precision cutoff weight (level + 1) child x ≤
          g.mass tops slope precision cutoff weight level (child / (g.branching : ℤ)) x := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid

15. theorem OAI.LipschitzHilbert.AngularGrid.path_mass_antitone line 127

    Source documentation

    Along any fixed top's angular path the actual mass is antitone.

    theorem path_mass_antitone (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
        (cutoff : ℝ) (weight : ι → X → ℝ) (hp : ∀ i ∈ tops, 0 ≤ precision i)
        (hw : ∀ i x, 0 ≤ weight i x) (top : ι) (x : X) :
        Antitone fun level => g.mass tops slope precision cutoff weight level (g.index level (slope top)) x := by
    …

    Mentions: OAI.LipschitzHilbert.AngularGrid