MovingTemplateHarmonicDiagonal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The restored diagonal under the original giant and regular priors

theorem OAI.Ostmann.movingTemplate_harmonic_diagonal_le line 15

Source documentation

The original harmonic product law pays the giant atom and a single factorial product-fibre cost. The frequency range contributes no cardinality factor, because the diagonal key includes the frequency itself.

theorem movingTemplate_harmonic_diagonal_le
    (P Pg : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPg : ∀ p ∈ Pg, p.Prime)
    (outside : List ℕ) (μ : ℕ → P → ℝ) (childBound pivotBound V : ℕ → ℕ)
    (F : MovingSlotState P → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
    (φ : ℝ → ℝ) (hφ0 : ∀ x, 0 ≤ φ x) (hφ1 : ∀ x, φ x ≤ 1) (G : ℕ → ℝ)
    (cg : ℝ)
    (n r m : ℕ) (Q : MovingRegularSlot n r m → Finset ℕ)
    (u : TreeLeafIndex n × Fin 4 → P) (p : ℕ)
    (hvg : ∀ q : Pg, V n < (q : ℕ)) (hvr : ∀ q : P, V n < (q : ℕ))
    (hsep : ∀ q : Pg, ∀ a : P, (q : ℕ) ≠ (a : ℕ))
    (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) :
    let A := Pg × ((MovingRegularSlot n r m → P) × transferFrequencyRange (V n))
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.transferFrequencyRange