TerminalPairComparison.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Comparing two generic terminal windows

This is the finite-test form of the shearing contradiction. Uniform closeness of the paired paths and two generic average estimates bound the actual measure-invariance defect. Neither path is assumed to stay in a compact set.

lemma OAI.DukePrimeDegree.normalized_interval_average_sub_bound line 21
lemma OAI.DukePrimeDegree.abs_sub_le_three_errors line 43
theorem OAI.DukePrimeDegree.terminal_pair_invarianceDefect_bound line 53

theorem OAI.DukePrimeDegree.no_terminal_pair_with_separated_defect line 80

Source documentation

A test separating a compact transverse shell contradicts paired genericity at error one quarter of that separation.

theorem no_terminal_pair_with_separated_defect {n : ℕ}
    (μ : Measure (X n))
    (f : CompactlySupportedContinuousMap (X n) ℝ) (h : G n)
    (p q : ℝ → X n) (hp : Continuous p) (hq : Continuous q)
    (δ T ε : ℝ) (hδ : 0 < δ) (hT : 0 < T) (hε : 0 < ε)
    (hsep : ε < |invarianceDefect μ f h|)
    (hleft : |(δ * T)⁻¹ * (∫ t in ((1 - δ) * T)..T,
      f (rightAction (p t) h)) - ∫ x, f (rightAction x h) ∂μ| ≤ ε / 4)
    (hright : |(δ * T)⁻¹ * (∫ t in ((1 - δ) * T)..T, f (q t)) -
      ∫ x, f x ∂μ| ≤ ε / 4)
    (hclose : ∀ t ∈ Icc ((1 - δ) * T) T,
      |f (rightAction (p t) h) - f (q t)| ≤ ε / 4) : False := by
…

Mentions: OAI.DukePrimeDegree.invarianceDefect