EnlargementCost.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Jacobian bounds for the enlarged full-dimensional simplex.

lemma OAI.TotientAsymptotic.triangular_sum line 14
lemma OAI.TotientAsymptotic.enlargementScale_le_exp line 34
theorem OAI.TotientAsymptotic.enlargement_jacobian_bound line 46
Source documentation
The accumulated Jacobian is controlled by the weighted perturbation sum.
```
theorem enlargement_jacobian_bound {N : ℕ} {β : ℕ → ℝ}
    (hβ : ∀ r, 1 ≤ β r) :
    (∏ i : Fin N, enlargementScale β i) ≤
      Real.exp (∑ r ∈ Finset.range N, ((N-r : ℕ) : ℝ)*(β r-1)) := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.enlargementScale

lemma OAI.TotientAsymptotic.reverse_perturbation_sum_le line 66

Source documentation

Perturbations indexed by distance from the top are charged only their remaining dimension, and can therefore be bounded by one convergent tail.

lemma reverse_perturbation_sum_le {m P : ℕ} (hPm : P ≤ m) (e : ℕ → ℝ)
    (he : ∀ h, 0 ≤ e h) (hsum : Summable (fun h : ℕ => (h : ℝ)*e h)) :
    (∑ r ∈ Finset.range (m-P), ((m-P-r : ℕ) : ℝ)*e (m-r)) ≤
      ∑' n : ℕ, ((P+n : ℕ) : ℝ)*e (P+n) := by
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.P

theorem OAI.TotientAsymptotic.reverse_enlargement_jacobian line 108

Source documentation

The actual reverse-indexed enlargement has a uniform full Jacobian.

theorem reverse_enlargement_jacobian {m P : ℕ} (hPm : P ≤ m)
    (e : ℕ → ℝ) (he : ∀ h, 0 ≤ e h)
    (hsum : Summable (fun h : ℕ => (h : ℝ)*e h)) :
    (∏ i : Fin (m-P), enlargementScale (fun r => 1+e (m-r)) i) ≤
      Real.exp (∑' n : ℕ, ((P+n : ℕ) : ℝ)*e (P+n)) := by
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.enlargementScale

theorem OAI.TotientAsymptotic.reverse_enlargement_coordinate line 120

Source documentation

Through the retained prefix, each individual scaling factor tends to one with the prefix cutoff, even when the full dimension grows.

theorem reverse_enlargement_coordinate {m H N : ℕ} (hHm : H ≤ m)
    (e : ℕ → ℝ) (he : ∀ h, 0 ≤ e h)
    (hsum : Summable (fun h : ℕ => (h : ℝ)*e h)) (i : Fin N)
    (hi : i.val < m-H) :
    enlargementScale (fun r => 1+e (m-r)) i ≤
      Real.exp (∑' n : ℕ, ((H+n : ℕ) : ℝ)*e (H+n)) := by
…

Mentions: OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.enlargementScale