Contradiction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.polynomialEpsilon line 15
Source documentation
Choose the uniform ε before any endpoint coefficient arrays are supplied.
```
noncomputable def polynomialEpsilon (K : ℕ) (D δ : ℝ) (hδ : 0 < δ) : ℝ :=
…
```
theorem OAI.FiniteFactor.polynomialEpsilon_pos line 18
def OAI.FiniteFactor.coefficientMass line 22
theorem OAI.FiniteFactor.polynomialEpsilon_le_mass line 25

theorem OAI.FiniteFactor.polynomial_event_integral_lower line 42

Source documentation

The finite-polynomial lower bound survives expectation on a measurable event, using only almost-everywhere coefficient bounds.

theorem polynomial_event_integral_lower (K : ℕ) (D δ : ℝ) (hδ : 0 < δ)
    (A B : Ω → ℤ → ℂ) {E : Set Ω} (hE : MeasurableSet E)
    (hint : IntegrableOn (fun ω => coefficientMass K (A ω) (B ω)) E μ)
    (hA : ∀ᵐ ω ∂μ, ω ∈ E →
      ∀ v : ℤ, -(K : ℤ) ≤ v → v ≤ K → ‖A ω v‖ ≤ D)
    (hB : ∀ᵐ ω ∂μ, ω ∈ E →
      ∀ v : ℤ, -(K : ℤ) ≤ v → v ≤ K → ‖B ω v‖ ≤ D)
    (hA0 : ∀ᵐ ω ∂μ, ω ∈ E → δ ≤ ‖A ω 0‖)
    (hB0 : ∀ᵐ ω ∂μ, ω ∈ E → δ ≤ ‖B ω 0‖) :
    polynomialEpsilon K D δ hδ * μ.real E ≤
      ∫ ω in E, coefficientMass K (A ω) (B ω) ∂μ := by
…

Mentions: OAI.FiniteFactor.coefficientMass, OAI.FiniteFactor.polynomialEpsilon

theorem OAI.FiniteFactor.coefficientMass_integral_upper line 64

Source documentation

Sum the per-coefficient expectation bounds over the exact finite range.

theorem coefficientMass_integral_upper (K : ℕ) (A B : Ω → ℤ → ℂ)
    {E : Set Ω} {a : ℝ}
    (hint : ∀ n ≤ 2*K, IntegrableOn
      (fun ω => ‖laurentProductCoefficient K (A ω) (B ω) (-(n : ℤ))‖) E μ)
    (hupper : ∀ n ≤ 2*K,
      (∫ ω in E, ‖laurentProductCoefficient K (A ω) (B ω) (-(n : ℤ))‖ ∂μ) ≤ a) :
    (∫ ω in E, coefficientMass K (A ω) (B ω) ∂μ) ≤ (2*(K : ℝ)+1)*a := by
…

Mentions: OAI.FiniteFactor.laurentProductCoefficient, OAI.FiniteFactor.coefficientMass

theorem OAI.FiniteFactor.exponential_tail_relaxation line 79

Source documentation

The numerical relaxation in final-upper-bound.

theorem exponential_tail_relaxation {L : ℝ} (hL : 0 ≤ L) :
    Real.exp (-L) + 2 * Real.exp (-L/800) ≤ 3 * Real.exp (-L/10000) := by
…

theorem OAI.FiniteFactor.no_eventual_small_convolutions line 85