ThickenedWitness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Thickening a discrete witness tail to its entire unit box preserves membership in the same controlled full-dimensional enlargement.

lemma OAI.TotientAsymptotic.thickened_witness_enclosure line 16
theorem OAI.TotientAsymptotic.eventually_thickened_witness_enclosure line 51
Source documentation
The prefix lower-bound hypothesis above is automatic uniformly over all witnesses and all prefix points once the tail cut is large.
```
theorem eventually_thickened_witness_enclosure (hren : FordRenewalInput) :
    ∀ᶠ H : ℕ in atTop, ∀ {x : ℝ} {η : TailDatum H},
      0 ≤ theta x → H ≤ m x → P H < H → 0 ≤ B x →
      1 ≤ B x*rho^(m x) → IsWitness H (theta x) η →
      ∀ {u : Fin (R x H) → ℝ}, u ∈ tailPrefixRegion x H η →
      ∀ {v : Fin (H-P H) → ℝ}, (∀ i, |tailVector η i-v i| ≤ 1) →
      joinCoordinates (R x H) (H-P H) (u,v) ∈
        enlargedSimplex (R x H+(H-P H)) (B x) (1+simplexBoxError 4 (m x))
          (fun i => 1+simplexBoxError 4 (m x-(i.val+1))) := by
…
```
Mentions: OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.tailVector, OAI.TotientAsymptotic.joinCoordinates, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.simplexBoxError