SupportedRegularInitialAmplitude.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Initial Poisson bounds on the actual support of the original prior

def OAI.Ostmann.priorSupportedWeight line 9
theorem OAI.Ostmann.priorSupportedWeight_support line 13
theorem OAI.Ostmann.priorSupportedWeight_sum line 20
theorem OAI.Ostmann.regularInitialAmplitude_priorSupportedWeight line 29

theorem OAI.Ostmann.regularInitialAmplitude_lower_on_support line 39

Source documentation

Product and frequency bounds need hold only where the original weighted summand is nonzero. Zero prior atoms are removed by an exact identity.

theorem regularInitialAmplitude_lower_on_support {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
    (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
    (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
    (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i)
    (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
    (hzero : ∀ i q, (∑ a, F i q a) = 0)
    (henergy : ∀ i q, (∑ a, ‖F i q a‖ ^ 2) ≤ q)
    (ψ : 𝓢(ℝ, ℂ)) (X H R Δ δ : ℝ) (hX : 0 < X) (hR : 0 < R) (N : ℕ)
    (w : (Fin n → P) → ℂ) (hw : ∀ x, ‖w x‖ ≤ 1)
    (hcut : ∀ x, productPrior μ x ≠ 0 → w x ≠ 0 → H * (∏ i, (x i : ℕ)) ≤ N * X)
    (hsupp : ∀ t : ℝ, H < |t| → 𝓕 ψ t = 0)
…

Mentions: OAI.Ostmann.productPrior