OAI/Analysis/LipschitzHilbert/Trees/SourceStoppedAmplitude.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.sourceNodeDenominator_ge_mass line 12
2. theorem OAI.LipschitzHilbert.sourceNodeDenominator_ge_child line 19
3. def OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathAmplitude line 34
4. def OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathDenominator line 45
5. theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_ratio_eq_amount_div_denominator line 59
6. theorem OAI.LipschitzHilbert.AngularGrid.source_active_path_eq_stopped_product line 75
7. theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_path_denominator_ge_next line 97

   Source documentation

   The true denominator controls the next distinguished path node, even when the path terminates while other children survive.

   theorem source_shifted_path_denominator_ge_next {Kb : ℕ} (g : AngularGrid) (tops : Finset τ)
       (slope precision : τ → ℝ) (cutoff : ℝ) (weight : τ → X → ℝ)
       (hprecision : ∀ t ∈ tops, 0 ≤ precision t) (hweight : ∀ t x, 0 ≤ weight t x)
       (K : ℕ) (gap : ℕ → ℝ) (packets : Finset σ) (assigned : σ → τ)
       (stop : σ → ℕ) (value : X → σ → EuclideanSpace ℂ κ)
       (phase : ℕ → ℂ) (a α p : ℝ) (hp : 0 < p) (hKb : 0 < Kb)
       (tag : Fin Kb) (top : τ) (htop : top ∈ tops) (x : X) (j : ℕ)
       (he : g.eligible cutoff (precision top) (ShiftedBlocks.endpoint tag j)) :
       let n := g.shiftedPathMass tops slope precision cutoff weight tag top x
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint