MovingTemplateLiveSymmetrization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The restored diagonal under the original giant and regular priors

theorem OAI.Ostmann.movingTemplate_symmetrized_harmonic_diagonal_live line 18

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_symmetrized_harmonic_diagonal_live
    (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 ℕ)
    (hν : ∀ j k : TreeLeafIndex n × Fin m,
      primeSubsetPrior P (Q (movingTemplateBulk n r m j)) =
        primeSubsetPrior P (Q (movingTemplateBulk n r m k)))
    (u : TreeLeafIndex n × Fin 4 → P) (p : ℕ)
    (hvg : ∀ q : Pg, smoothGiantPrior Pg φ cg q ≠ 0 → V n < (q : ℕ)) (hvr : ∀ i (q : P), primeSubsetPrior P (Q i) q ≠ 0 → V n < (q : ℕ))
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.movingTemplateBulk, OAI.Ostmann.smoothGiantPrior