OAI/NumberTheory/Ostmann/Construction/PositiveWordStatistic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.wordStatisticTerm line 13
2. theorem OAI.Ostmann.wordStatisticTerm_nonneg line 17
3. theorem OAI.Ostmann.wordStatisticTerm_summable line 24
4. theorem OAI.Ostmann.wordStatistic_lower line 46

   Source documentation

   The selected endpoints give a lower bound for the full positive statistic, with all cell multiplicities retained.

   theorem wordStatistic_lower {m : ℕ} (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
       (G : ℤ → ℂ) (R : Fin m → ℤ → ℂ) (S : Finset ℤ)
       (hψ : ∀ x, 0 ≤ (ψ x).re) (hG : ∀ a, ‖G a‖ ≤ 1) (hR : ∀ i a, ‖R i a‖ ≤ 1)
       (c u δ : ℝ) (hu : 0 ≤ u) (hδ : 0 ≤ δ)
       (hcS : ∀ a ∈ S, c ≤ (ψ ((a : ℝ) / X)).re)
       (huS : ∀ a ∈ S, u ≤ ‖G a‖) (hδS : ∀ a ∈ S, ∀ i, δ ≤ ‖R i a‖) :
       S.card * (c * u ^ 2 * δ ^ (2 * m)) ≤ ∑' a : ℤ, wordStatisticTerm ψ X G R a := by
   …

   Mentions: OAI.Ostmann.wordStatisticTerm