PhysicalMomentLower.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Jensen amplification of the actual translated-character biases

theorem OAI.Ostmann.ternaryMean_sum_lower line 12
theorem OAI.Ostmann.finite_even_moment_lower line 23

theorem OAI.Ostmann.weighted_finite_bias_moment line 43

Source documentation

Positive weight on a finite endpoint tail amplifies its simultaneous individual prime biases. The moment on the right is an actual infinite sum.

theorem weighted_finite_bias_moment {ι A : Type*} [Fintype A]
    (S : Finset ι) (w : ι → ℝ) (y : ι → A → ℝ) (c w₀ : ℝ)
    (k : ℕ) (heven : Even k) (hA : 0 < Fintype.card A)
    (hc : 0 ≤ c) (hw₀ : 0 ≤ w₀) (hw : ∀ i, 0 ≤ w i)
    (hwS : ∀ i ∈ S, w₀ ≤ w i) (hws : Summable w)
    (hy : ∀ i a, y i a = 0 ∨ y i a = 1 ∨ y i a = -1)
    (hbias : ∀ a, (S.card : ℝ) * c ≤ ∑ i ∈ S, y i a) :
    w₀ * S.card * c ^ k ≤ ∑' i, w i * ternaryMean (y i) ^ k := by
…

Mentions: OAI.Ostmann.ternaryMean