BoundedWordStatistic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The initial positive statistic with its actual finite physical bounds

theorem OAI.Ostmann.wordStatisticTerm_summable_of_bounded line 12

Source documentation

The inverse giant transform need not have norm at most one. Only a finite bound is needed to sum its Schwartz-weighted physical statistic.

theorem wordStatisticTerm_summable_of_bounded {m : ℕ}
    (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
    (G : ℤ → ℂ) (R : Fin m → ℤ → ℂ) (CG : ℝ) (CR : Fin m → ℝ)
    (hψ : ∀ x, 0 ≤ (ψ x).re)
    (hG : ∀ a, ‖G a‖ ≤ CG) (hR : ∀ i a, ‖R i a‖ ≤ CR i) :
    Summable (wordStatisticTerm ψ X G R) := by
…

Mentions: OAI.Ostmann.wordStatisticTerm

theorem OAI.Ostmann.endpoint_mean_sq_le line 40

Source documentation

Cauchy--Schwarz converts a positive empirical mean into the squared norm needed for the original statistic, without pointwise positivity of the giant.

theorem endpoint_mean_sq_le {ι : Type*} (E : Finset ι) (G : ι → ℂ)
    (δ : ℝ) (hδ : 0 ≤ δ)
    (hmean : (E.card : ℝ) * δ ≤ ∑ a ∈ E, (G a).re) :
    (E.card : ℝ) * δ ^ 2 ≤ ∑ a ∈ E, ‖G a‖ ^ 2 := by
…

theorem OAI.Ostmann.wordStatistic_lower_of_endpoint_mean line 61

Source documentation

The selected endpoint mean feeds the whole statistic. No pointwise bound of one and no pointwise lower bound on the giant function is imposed.

theorem wordStatistic_lower_of_endpoint_mean {m : ℕ}
    (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
    (G : ℤ → ℂ) (R : Fin m → ℤ → ℂ) (E : Finset ℤ)
    (CG : ℝ) (CR : Fin m → ℝ)
    (hψ : ∀ x, 0 ≤ (ψ x).re)
    (hG : ∀ a, ‖G a‖ ≤ CG) (hR : ∀ i a, ‖R i a‖ ≤ CR i)
    (c δ γ : ℝ) (hc : 0 ≤ c) (hδ : 0 ≤ δ) (hγ : 0 ≤ γ)
    (hcE : ∀ a ∈ E, c ≤ (ψ ((a : ℝ) / X)).re)
    (hmean : (E.card : ℝ) * δ ≤ ∑ a ∈ E, (G a).re)
    (hγE : ∀ a ∈ E, ∀ i, γ ≤ ‖R i a‖) :
    (E.card : ℝ) * (c * δ ^ 2 * γ ^ (2 * m)) ≤
      ∑' a : ℤ, wordStatisticTerm ψ X G R a := by
…

Mentions: OAI.Ostmann.wordStatisticTerm