PrefixProjection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Projection preserves the nonnegative simplex inequalities.

lemma OAI.TotientAsymptotic.sum_restrict_le line 13
lemma OAI.TotientAsymptotic.enlargedSimplex_project line 24
def OAI.TotientAsymptotic.tupleInnerPrefix line 41
lemma OAI.TotientAsymptotic.tupleInnerPrefix_eq line 44
lemma OAI.TotientAsymptotic.tupleInnerPrefix_geometry line 62
Source documentation
Every inner prefix of an actual tuple retains all the projected bands and simplex inequalities; the removed suffix terms were nonnegative.
```
lemma tupleInnerPrefix_geometry {x t : ℝ} {H K : ℕ} (hPH : P H ≤ H)
    (hn : R x K ≤ R x H) (hL : 0 < L x H)
    {τ : TotientTuple (R x H)} (hτ : IsBasicTuple x H t τ) :
    (∀ j, (tupleInnerPrefix τ (R x K) j).Prime) ∧
    primePrefixCoord (tupleInnerPrefix τ (R x K)) ∈ prefixBandRegion x K ∧
    primePrefixCoord (tupleInnerPrefix τ (R x K)) ∈
      enlargedSimplex (R x K) (B x) (xi x 0) (fun j => xi x (j.val+1)) := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.tupleInnerPrefix, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.xi