OAI/Analysis/LipschitzHilbert/Phase/AngularConservation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.AngularGrid.continuingTops line 17
2. def OAI.LipschitzHilbert.AngularGrid.children line 23
3. theorem OAI.LipschitzHilbert.AngularGrid.child_parent line 29
4. theorem OAI.LipschitzHilbert.AngularGrid.continuing_fiber line 38
5. theorem OAI.LipschitzHilbert.AngularGrid.sum_child_mass line 59

   Source documentation

   The next-level child masses partition precisely the continuing tops.

   theorem sum_child_mass (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ)
       (cutoff : ℝ) (weight : ι → X → ℝ) (hp : ∀ i ∈ tops, 0 ≤ precision i)
       (level : ℕ) (cell : ℤ) (x : X) :
       (∑ child ∈ g.children tops slope precision cutoff level cell,
         g.mass tops slope precision cutoff weight (level + 1) child x) =
           ∑ i ∈ g.continuingTops tops slope precision cutoff level cell, weight i x := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

6. theorem OAI.LipschitzHilbert.AngularGrid.parent_mass_conservation line 82

   Source documentation

   The actual parent mass splits into next-level child masses and the positive weights of tops whose eligibility stops at this level.

   theorem parent_mass_conservation (g : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
       (hp : ∀ i ∈ tops, 0 ≤ precision i) (level : ℕ) (cell : ℤ) (x : X) :
       g.mass tops slope precision cutoff weight level cell x =
         (∑ child ∈ g.children tops slope precision cutoff level cell,
           g.mass tops slope precision cutoff weight (level + 1) child x) +
         ∑ i ∈ (g.cellTops tops slope precision cutoff level cell).filter
           (fun i => ¬g.eligible cutoff (precision i) (level + 1)), weight i x := by
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid