OAI/NumberTheory/Ostmann/Construction/BinnedWordNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute endpoint means suffice for selecting the original character bin

  1. theorem OAI.Ostmann.binnedWordAverage_total_norm_lower line 9
  2. theorem OAI.Ostmann.common_large_word_bin_of_norm line 19

    Source documentation

    This pigeonhole fixes the bin before the endpoint-dependent cell lists.

    theorem common_large_word_bin_of_norm {A B : Type*} [Fintype A] [Fintype B] [Nonempty B]
    {n : ℕ} (E : Finset ℕ) (μ : Fin n → A → ℝ) (F : ℕ → Fin n → A → ℂ)
    (bin : (Fin n → A) → B) (δ : ℝ) (hδ : 0 ≤ δ)
    (hmean : ∀ a ∈ E, ∀ i, δ ≤ ‖∑ p, (μ i p : ℂ) * F a i p‖) :
    ∃ b, ∃ S : Finset ℕ, S ⊆ E ∧ E.card ≤ Fintype.card B * S.card ∧
      ∀ a ∈ S, δ ^ n ≤ (Fintype.card B : ℝ) * ‖binnedWordAverage μ (F a) bin b‖ := by
…

    Mentions: OAI.Ostmann.binnedWordAverage