OAI/NumberTheory/Ostmann/Construction/FiniteCellMeans.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.finiteCellMass line 11
2. def OAI.Ostmann.finiteCellMean line 14
3. theorem OAI.Ostmann.finiteCellMass_nonneg line 17
4. theorem OAI.Ostmann.finiteCellMass_mul_mean line 21
5. theorem OAI.Ostmann.finiteCellMean_le_one line 32
6. theorem OAI.Ostmann.finiteCellMass_sum line 45
7. theorem OAI.Ostmann.finiteCellMean_sum line 50
8. theorem OAI.Ostmann.finite_positive_heavy_cells line 59

   Source documentation

   A positive average over the primes yields many heavy cells of positive average under the actual fiber masses, without a new probabilistic input.

   theorem finite_positive_heavy_cells (P I : Finset ℕ) (label : ℕ → ℕ) (μ f : ℕ → ℝ)
       (hlabel : ∀ p ∈ P, label p ∈ I) (hμ : ∀ p ∈ P, 0 ≤ μ p)
       (hf : ∀ p ∈ P, f p ≤ 1) (δ θ M : ℝ) (hδ : 0 ≤ δ) (hθ : 0 ≤ θ)
       (hbias : δ * (∑ p ∈ P, μ p) ≤ ∑ p ∈ P, μ p * f p)
       (hthin : I.card * θ ≤ (δ / 4) * ∑ p ∈ P, μ p)
       (hcap : ∀ h ∈ I, finiteCellMass P label μ h ≤ M) :
       (δ / 4) * (∑ p ∈ P, μ p) ≤
         (positiveHeavyCells I (finiteCellMass P label μ) (finiteCellMean P label μ f) δ θ).card * M := by
   …

   Mentions: OAI.Ostmann.finiteCellMass, OAI.Ostmann.positiveHeavyCells, OAI.Ostmann.finiteCellMean