InitialWordLowerBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

From positive endpoint means to the initial word statistic

theorem OAI.Ostmann.initial_word_lower_bound line 13

Source documentation

The product-bin and endpoint pigeonholes feed the full nonnegative Schwartz-weighted statistic.

theorem initial_word_lower_bound {A B : Type*} [Fintype A] [Fintype B] [Nonempty B]
    {k m : ℕ} (E : Finset ℕ) (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
    (μ : Fin k → A → ℝ) (F : ℤ → Fin k → A → ℂ)
    (bin : (Fin k → A) → B) (R : Fin m → ℤ → ℂ)
    (hμ : ∀ i x, 0 ≤ μ i x) (hmass : ∀ i, ∑ x, μ i x = 1)
    (hF : ∀ a i x, ‖F a i x‖ ≤ 1) (hR : ∀ i a, ‖R i a‖ ≤ 1)
    (c δ γ : ℝ) (hc : 0 ≤ c) (hδ : 0 ≤ δ) (hγ : 0 ≤ γ)
    (hψ : ∀ x, 0 ≤ (ψ x).re)
    (hcE : ∀ a ∈ E, c ≤ (ψ ((a : ℝ) / X)).re)
    (hmean : ∀ a ∈ E, ∀ i, δ ≤ (∑ x, (μ i x : ℂ) * F a i x).re)
    (hcell : ∀ a ∈ E, ∀ i, γ ≤ (R i a).re) :
    ∃ b : B,
…