FactorialMajorant.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Factorial weights for the inverse-jet estimate

We use the fixed admissible Gevrey exponent σ = 2. The weight L m = (m + 1) * ((m + 1)!)² is positive, has L 0 = 1, and its normalized interior convolution tends to zero. Consequently the abstract inverse majorant gives one constant for every derivative order.

def OAI.RegularPointCoordinates.factorialMajorant line 24
theorem OAI.RegularPointCoordinates.factorialMajorant_zero line 27
theorem OAI.RegularPointCoordinates.factorialMajorant_one line 30
theorem OAI.RegularPointCoordinates.factorialMajorant_pos line 33
theorem OAI.RegularPointCoordinates.factorialMajorant_succ line 37
theorem OAI.RegularPointCoordinates.factorialMajorant_pair_step line 45
Source documentation
The consecutive ratios of the weight are increasing.
```
theorem factorialMajorant_pair_step {p q : ℕ} (hpq : p ≤ q) :
    factorialMajorant (p + 1) * factorialMajorant q ≤
      factorialMajorant p * factorialMajorant (q + 1) := by
…
```
Mentions: OAI.RegularPointCoordinates.factorialMajorant
theorem OAI.RegularPointCoordinates.factorialMajorant_pair_le_endpoint line 65
Source documentation
For fixed total order, the largest positive-order product is at an endpoint.
```
theorem factorialMajorant_pair_le_endpoint {l q : ℕ} (hl : 1 ≤ l) (hq : 1 ≤ q) :
    factorialMajorant l * factorialMajorant q ≤
      factorialMajorant 1 * factorialMajorant (l + q - 1) := by
…
```
Mentions: OAI.RegularPointCoordinates.factorialMajorant
theorem OAI.RegularPointCoordinates.factorialMajorant_endpoint_ratio line 85
theorem OAI.RegularPointCoordinates.factorialMajorant_normalized_convolution_le line 103
Source documentation
A direct bound sufficient for convolution decay.
```
theorem factorialMajorant_normalized_convolution_le (m : ℕ) :
    normalizedInteriorConvolution factorialMajorant m ≤ 8 / ((m : ℝ) + 1) := by
…
```
Mentions: OAI.RegularPointCoordinates.normalizedInteriorConvolution, OAI.RegularPointCoordinates.factorialMajorant
theorem OAI.RegularPointCoordinates.factorialMajorant_convolution_tendsto_zero line 139
theorem OAI.RegularPointCoordinates.factorialMajorant_full_convolution_le line 150
Source documentation
Restoring the endpoint terms gives the uniform full-convolution estimate.
```
theorem factorialMajorant_full_convolution_le (m : ℕ) :
    (∑ l ∈ Finset.range (m + 1), factorialMajorant l * factorialMajorant (m - l)) ≤
      10 * factorialMajorant m := by
…
```
Mentions: OAI.RegularPointCoordinates.factorialMajorant
theorem OAI.RegularPointCoordinates.factorial_inverse_coefficients_uniform_bound line 182
Source documentation
The factorial weights satisfy the inverse-coefficient bound with one constant, uniformly over all orders and all admissible coefficient sequences.
```
theorem factorial_inverse_coefficients_uniform_bound {A : ℝ} (hA : 1 ≤ A) :
    ∃ C : ℝ, Real.sqrt A ≤ C ∧ 2 * A ≤ C ∧
      ∀ a : ℕ → ℝ, a 0 ≤ Real.sqrt A →
        HasInverseMajorantRecurrence factorialMajorant a A →
        ∀ m, a m ≤ C * factorialMajorant m :=
…
```
Mentions: OAI.RegularPointCoordinates.HasInverseMajorantRecurrence, OAI.RegularPointCoordinates.factorialMajorant