OAI/NumberTheory/Ostmann/Construction/PositiveWordBins.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.binnedWordAverage line 13
2. theorem OAI.Ostmann.binnedWordAverage_sum line 17
3. theorem OAI.Ostmann.binnedWordAverage_total_lower line 28

   Source documentation

   Independent positive real means give a large total word mean before choosing any product bin.

   theorem binnedWordAverage_total_lower {A B : Type*} [Fintype A] [Fintype B] {n : ℕ}
       (μ : Fin n → A → ℝ) (F : Fin n → A → ℂ) (bin : (Fin n → A) → B)
       (δ : ℝ) (hδ : 0 ≤ δ) (hmean : ∀ i, δ ≤ (∑ a, (μ i a : ℂ) * F i a).re) :
       δ ^ n ≤ ‖∑ b, binnedWordAverage μ F bin b‖ := by
   …

   Mentions: OAI.Ostmann.binnedWordAverage

4. theorem OAI.Ostmann.exists_large_complex_bin line 40

   Source documentation

   A finite product-bin partition retains a large coefficient in at least one bin.

   theorem exists_large_complex_bin {B : Type*} [Fintype B] [Nonempty B]
       (v : B → ℂ) : ∃ b, ‖∑ j, v j‖ ≤ (Fintype.card B : ℝ) * ‖v b‖ := by
   …

5. theorem OAI.Ostmann.exists_large_word_bin line 48
6. theorem OAI.Ostmann.common_large_bin line 56

   Source documentation

   A single bin works on a proportionate set of the actual endpoints.

   theorem common_large_bin {B : Type*} [Fintype B] [Nonempty B]
       (E : Finset ℕ) (v : ℕ → B → ℂ) (η : ℝ)
       (hE : ∀ a ∈ E, η ≤ ‖∑ b, v a b‖) :
       ∃ b, ∃ S : Finset ℕ, S ⊆ E ∧ E.card ≤ Fintype.card B * S.card ∧
         ∀ a ∈ S, η ≤ (Fintype.card B : ℝ) * ‖v a b‖ := by
   …

7. theorem OAI.Ostmann.binnedWordAverage_norm_le_one line 79

   Source documentation

   Every bin coefficient remains bounded by one under the original probability law; restricting a bin does not renormalize that law.

   theorem binnedWordAverage_norm_le_one {A B : Type*} [Fintype A] {n : ℕ}
       (μ : Fin n → A → ℝ) (F : Fin n → A → ℂ) (bin : (Fin n → A) → B) (b : B)
       (hμ : ∀ i a, 0 ≤ μ i a) (hmass : ∀ i, ∑ a, μ i a = 1)
       (hF : ∀ i a, ‖F i a‖ ≤ 1) : ‖binnedWordAverage μ F bin b‖ ≤ 1 := by
   …

   Mentions: OAI.Ostmann.binnedWordAverage