JoinedSimplex.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact full-dimensional completion of a continuous prefix by its discrete tail.

lemma OAI.TotientAsymptotic.joined_prefix_row line 15
lemma OAI.TotientAsymptotic.joined_tail_row line 30
lemma OAI.TotientAsymptotic.joined_budget line 46
lemma OAI.TotientAsymptotic.prefix_D_tailVector line 52
lemma OAI.TotientAsymptotic.top_D_tailVector line 65
theorem OAI.TotientAsymptotic.join_witness_enlarged line 78
Source documentation
No prefix prime bands are required for exact completion to the full simplex: the unperturbed prefix constraints and the witness tail suffice.
```
theorem join_witness_enlarged {x : ℝ} {H : ℕ} {η : TailDatum H}
    (hη : IsWitness H (theta x) η) (hPH : P H < H) (hHm : H ≤ m x) (hB : 0 ≤ B x)
    {u : Fin (R x H) → ℝ} (hu : u ∈ tailPrefixRegion x H η) :
    joinCoordinates (R x H) (H-P H) (u,tailVector η) ∈
      enlargedSimplex (R x H+(H-P H)) (B x) (xi x 0) (fun i => xi x (i.val+1)) := by
…
```
Mentions: OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tailPrefixRegion, OAI.TotientAsymptotic.joinCoordinates, OAI.TotientAsymptotic.tailVector, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.xi