HalfPrimeEndpoint.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The common endpoint scalar in the Section 7 half-list

def OAI.Ostmann.endpointResidueValue line 10
theorem OAI.Ostmann.normalizedResidueIndicator_endpoint line 13
theorem OAI.Ostmann.endpointResidueValue_nonneg line 19
theorem OAI.Ostmann.endpointResidueValue_balanced line 29
Source documentation
A fixed absolute lower bound suffices for the exponential half-list loss.
```
theorem endpointResidueValue_balanced {p : ℕ} (S : Finset (ZMod p))
    (hlo : (1 / 3 : ℝ) ≤ residueDensity S) (hhi : residueDensity S ≤ 2 / 3) :
    (1 / 2 : ℝ) ≤ endpointResidueValue S := by
…
```
Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.endpointResidueValue
theorem OAI.Ostmann.halfPrimeScalar_nonneg line 45

theorem OAI.Ostmann.halfPrimeMean_giant_endpoint_lower line 56

Source documentation

The endpoint mean of the actual giant, and the balanced weighted event for the nongiant slots, give the doubled original-prior physical lower bound. The cutoffs remain inside the half-list weight.

theorem halfPrimeMean_giant_endpoint_lower {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)]
    (μ₀ : P → ℝ) (μ : Fin n → P → ℝ)
    (F₀ : (q : P) → ZMod (q : ℕ) → ℂ)
    (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
    (w : (Fin n → P) → ℝ) (cval : Fin n → P → ℝ)
    (hμ : ∀ i q, 0 ≤ μ i q) (hw : ∀ x, 0 ≤ w x)
    (hcval : ∀ i q, 0 ≤ cval i q)
    (hF₀ : ∀ q a, (F₀ q a).im = 0) (hF : ∀ i q a, (F i q a).im = 0)
    (E : Finset ℤ) (S : Finset (Fin n → P)) (β γ δ c : ℝ)
    (hβ : 0 ≤ β) (hγ : 0 ≤ γ) (hδ : 0 ≤ δ) (hc : 0 ≤ c)
    (hmass : β ≤ ∑ x ∈ S, productPrior μ x * w x)
…

Mentions: OAI.Ostmann.productPrior