SourceMassStopping.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The actual finite mass stopping index. A terminal ineligible top has zero path mass, so the source cutoff is attained without a positive lower bound on any individual top weight.

def OAI.LipschitzHilbert.firstMassStop line 15
theorem OAI.LipschitzHilbert.firstMassStop_spec line 18
theorem OAI.LipschitzHilbert.firstMassStop_after line 30
theorem OAI.LipschitzHilbert.firstMassStop_active_iff line 35

theorem OAI.LipschitzHilbert.measurable_firstMassStop line 46

Source documentation

Measurability follows from the actual active-mass events, so the source stopping indicator can be inserted into its packet factors.

theorem measurable_firstMassStop {X : Type*} [MeasurableSpace X]
    (n : X → ℕ → ℝ) (count : ℕ) (M : ℝ)
    (hn : ∀ j, Measurable (fun x => n x j))
    (hlast : ∀ x, n x count ≤ M) (hanti : ∀ x, Antitone (n x)) :
    Measurable (fun x => firstMassStop (n x) count M) := by
…

Mentions: OAI.LipschitzHilbert.firstMassStop

theorem OAI.LipschitzHilbert.AngularGrid.measurable_shiftedPathMass line 61
theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_terminal_zero line 72
theorem OAI.LipschitzHilbert.AngularGrid.exists_shifted_terminal line 81
Source documentation
One common finite terminal generation works for every point: the chosen top has become ineligible there, independently of its weight.
```
theorem exists_shifted_terminal {K : ℕ} (g : AngularGrid) (cutoff precision : ℝ)
    (hp : 0 < precision) (hK : 0 < K) (σ : Fin K) :
    ∃ count : ℕ, ¬g.eligible cutoff precision (ShiftedBlocks.endpoint σ count) := by
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint

theorem OAI.LipschitzHilbert.AngularGrid.shifted_mass_stopping line 91

Source documentation

The source stopped mass path is an initial segment of the original angular path. The final mass may vanish, and all later masses are at most M.

theorem shifted_mass_stopping {ι X : Type*} {K : ℕ}
    (g : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ) (cutoff : ℝ)
    (weight : ι → X → ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (hw : ∀ t x, 0 ≤ weight t x) (hK : 0 < K)
    (σ : Fin K) (top : ι) (htop : top ∈ tops) (count : ℕ)
    (hterminal : ¬g.eligible cutoff (precision top) (ShiftedBlocks.endpoint σ count))
    (M : ℝ) (hM : 0 ≤ M) (x : X) :
    let n := g.shiftedPathMass tops slope precision cutoff weight σ top x
…

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

theorem OAI.LipschitzHilbert.AngularGrid.measurable_shiftedMassStop line 116