BoundaryEnclosure.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A box crossing a witness-region boundary meets a retained slack slice or a fixed-deviation band exceptional set.

lemma OAI.TotientAsymptotic.join_witness_band_lower line 15
lemma OAI.TotientAsymptotic.witness_full_cube_enclosure line 29
lemma OAI.TotientAsymptotic.exact_failure_shell line 54
lemma OAI.TotientAsymptotic.band_endpoint_neighborhood line 96

theorem OAI.TotientAsymptotic.witness_boundary_enclosure line 118

Source documentation

Every point in a crossing box belongs to one of the two already controlled full-dimensional exceptional regions.

theorem witness_boundary_enclosure {x : ℝ} {H : ℕ} {η : TailDatum H}
    (hs : 0 ≤ theta x) (hB : 0 ≤ B x) (hcut : 4 ≤ lam*(P H : ℝ))
    (hP : 1 ≤ P H) (hPH : P H < H) (hHm : H ≤ m x)
    (hBr : 1 ≤ B x*rho^(m x)) (hη : IsWitness H (theta x) η)
    (hlarge : ∀ i : Fin (R x H), 100 < bandScale x (i.val+1))
    {u u₀ w : Fin (R x H) → ℝ}
    (hu₀ : u₀ ∈ perturbedTailPrefixRegion x H η ∩ prefixBandRegion x H)
    (hu : ∀ i, |u₀ i-u i| ≤ 1)
    (hw : w ∉ perturbedTailPrefixRegion x H η ∩ prefixBandRegion x H)
    (hwu : ∀ i, |w i-u i| ≤ 1) {v : Fin (H-P H) → ℝ}
    (hv : ∀ i, |tailVector η i-v i| ≤ 1) :
    joinCoordinates (R x H) (H-P H) (u,v) ∈
…

Mentions: OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.w, OAI.TotientAsymptotic.perturbedTailPrefixRegion, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.tailVector, OAI.TotientAsymptotic.joinCoordinates