PrefixCoordinates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinates of the triangular prefix simplex in its slack variables.

lemma OAI.TotientAsymptotic.prefixSlack_shift line 10
lemma OAI.TotientAsymptotic.prefix_coordinate_slacks line 27
lemma OAI.TotientAsymptotic.prefix_coordinate_full_sum line 33
theorem OAI.TotientAsymptotic.prefixLinear_coordinate line 56
Source documentation
The inverse of the determinant-one triangular slack map.
```
theorem prefixLinear_coordinate (N : ℕ) (u : Fin N → ℝ) (i : Fin N) :
    u i = ∑ j : Fin N,
      if i ≤ j then g (j.val-i.val)*prefixLinear N u j else 0 := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.g, OAI.TotientAsymptotic.prefixLinear