StoppingScaleIntervals.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Stopping-level bands are intervals of the original source length index. This is the bridge from interval concentration to summation by parts over angular stopping levels.

theorem OAI.LipschitzHilbert.antitone_stopping_band_interval line 17

theorem OAI.LipschitzHilbert.sum_stopping_fibers line 52

Source documentation

Summing fibers of the actual stopping map loses neither packets nor multiplicity.

theorem sum_stopping_fibers {N : ℕ} {E : Type*} [AddCommMonoid E]
    (stop : Fin N → ℕ) (f : Fin N → E) (a b : ℕ) :
    (∑ k ∈ Finset.Ico a b, ∑ j ∈ Finset.univ.filter (fun j => stop j = k), f j) =
      ∑ j ∈ Finset.univ.filter (fun j => a ≤ stop j ∧ stop j < b), f j := by
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.length_antitone line 75
theorem OAI.LipschitzHilbert.SourceLabeledLattice.precision_monotone line 81
theorem OAI.LipschitzHilbert.SourceLabeledLattice.stopping_antitone line 86
def OAI.LipschitzHilbert.SourceLabeledLattice.rawBand line 95
theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval_eq_band_sum line 101

theorem OAI.LipschitzHilbert.SourceLabeledLattice.stopping_band_eq_rawInterval line 115

Source documentation

Every partial sum over a band of angular stopping levels is one of the source intervals already controlled by the concentration theorem.

theorem stopping_band_eq_rawInterval (P : SourceLabeledLattice N κ Label Item)
    (coeff : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (i : Fin 3) (stop : Fin N → ℕ) (hstop : Antitone stop)
    (a b : ℕ) (x y : ℝ) :
    ∃ lower upper : ℕ, lower ≤ upper ∧ upper ≤ N ∧
      (∑ j ∈ Finset.univ.filter (fun j => a ≤ stop j ∧ stop j < b),
        P.rawBand coeff i j x y) = P.rawInterval coeff i lower upper x y := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice