Exponential.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The homogeneous expansion of an ordered exponential product, with factorial weights and multiplication order retained.

def OAI.Generator.exponentialDegree line 19
theorem OAI.Generator.exponentialDegree_zero line 24
theorem OAI.Generator.exponentialDegree_one line 29

theorem OAI.Generator.exponentialDegree_map line 36

Source documentation

Transport the finite original-degree polynomial through an algebra map.

theorem exponentialDegree_map {S : Type*} [Ring S] [Algebra ℝ S]
    (φ : R →ₐ[ℝ] S) (xs : List R) (d : ℕ) :
    φ (exponentialDegree xs d) = exponentialDegree (xs.map φ) d := by
…

Mentions: OAI.Generator.exponentialDegree

theorem OAI.Generator.exponentialDegree_summable_norm line 48
Source documentation
Absolute convergence for fixed row count. This is not the uniform bound.
```
theorem exponentialDegree_summable_norm (xs : List R) :
    Summable (fun d => ‖exponentialDegree xs d‖) := by
…
```
Mentions: OAI.Generator.exponentialDegree
theorem OAI.Generator.exponentialDegree_hasSum line 65
Source documentation
The series sums to the ordered product, without requiring commuting rows.
```
theorem exponentialDegree_hasSum (xs : List R) :
    HasSum (exponentialDegree xs) ((xs.map NormedSpace.exp).prod) := by
…
```
Mentions: OAI.Generator.exponentialDegree
theorem OAI.Generator.geometric_second_order_remainder line 81

theorem OAI.Generator.perturbation_remainder_from_degree_bounds line 93

Source documentation

The source's 4α²/(1−2α) expression, with precisely 0 < α < 1/2.

theorem perturbation_remainder_from_degree_bounds {α : ℝ} (hα : 0 < α) (hhalf : α < 1 / 2)
    (f : ℕ → E) {S : E} (hs : HasSum f S)
    (hb : ∀ n : ℕ, ‖f (n + 2)‖ ≤ (2 * α) ^ (n + 2)) :
    ‖S - f 0 - f 1‖ ≤ 4 * α ^ 2 / (1 - 2 * α) := by
…