MovingTemplateSupportedTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The full giant-prior step with its actual supported product bound

theorem OAI.Ostmann.movingTemplate_prior_transfer_on_support line 25

Source documentation

The support fields in the full Fourier transfer follow from the original coefficient. Compensation retains its original independent law; α contains the surviving external priors.

theorem movingTemplate_prior_transfer_on_support {σ A : Type} [Fintype σ] [Fintype A]
    (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime)
    (outside : List ℕ) (μ : ℕ → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
    (P I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hPI : P ⊆ I)
    (hI : ∀ p ∈ I, 0 < p) (hφ : ∀ x, 0 ≤ φ x)
    (hpos : 0 < smoothGiantMass P φ (G (n + 1)))
    (hμ : ∀ a, 0 ≤ μ n a) (hμmass : ∑ a, μ n a = 1)
    (X : A → ℕ) (hX : ∀ a, (X a).Prime)
    (y : A → MovingRegularSlot n r m → σ) (v : A → ℤ) (α : A → ℂ)
    (sets : ∀ q : ℕ, Finset (ZMod q))
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.MovingRegularSlot