OAI/NumberTheory/Ostmann/Construction/TailGiantEndpointStatistic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The selected giant mean as the actual initial endpoint sum

  1. theorem OAI.Ostmann.tailGiantPhysical_eq_primePhysicalTest line 11
  2. theorem OAI.Ostmann.tailGiantEndpointMean_weighted_sum line 20
  3. theorem OAI.Ostmann.tailGiantEndpointMean_endpoint_lower line 39

    Source documentation

    A selected full-cell mean is a positive sum over the literal integer endpoint set used in the initial Poisson statistic.

    theorem tailGiantEndpointMean_endpoint_lower (A : Set ℕ) (N : ℕ) (F E P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (μ : P → ℝ) (δ : ℝ)
    (hE : E.Nonempty) (hmean : δ ≤ ∑ p : P, μ p * tailGiantEndpointMean A N F E p) :
    let _ : ∀ p : P, Fact (p : ℕ).Prime := fun p => ⟨hP p p.property⟩
…

    Mentions: OAI.Ostmann.tailGiantEndpointMean