AngularSnapshot.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fourier prediction with actual snapshot masses and one path exception.

theorem OAI.LipschitzHilbert.AngularGrid.sum_cell_mass_le_ancestor line 18

theorem OAI.LipschitzHilbert.AngularGrid.snapshot_prediction_average line 41

Source documentation

The exact snapshot prediction of §9. The cardinality hypothesis concerns significant tops, not graph cells; one unshrunk path child is allowed without a significant representative. Both graph masses and normalized child weights are the finite sums of the actual positive top weights.

theorem snapshot_prediction_average {ι κ : Type*} [DecidableEq ι] [Fintype κ]
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox) (d : ι → ℝ)
    (cutoff : ℝ) (weight : ι → (ℝ × ℝ) → ℝ)
    (hd : ∀ i ∈ tops, 0 ≤ d i) (hw : ∀ i x, 0 < weight i x)
    (z : ℝ × ℝ) (base level : ℕ) (hle : base ≤ level)
    (parent : ℤ) (cells : Finset ℤ) (representative : cells → ℝ)
    (hcell : ∀ c, g.index (level + 1) (representative c) = c.val)
    (hancestor : ∀ c, g.index base (representative c) = parent)
    (hnonempty : ∀ c : cells,
      (g.cellTops tops (fun i => (T i).slope) d cutoff (level + 1) c.val).Nonempty)
    (exception : ℤ) {gap B K D p etaMin : ℝ}
    (hgap : 0 < gap) (hetaMin : 0 < etaMin) (hD : 2 ≤ D) (hp : 4 ≤ p)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox