InverseMajorant.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

An inverse-coefficient majorant without exponential loss

The normalized interior convolution of a positive weight sequence tends to zero. This makes the inverse recurrence contractive at large orders. Finite initial orders are bounded uniformly over every sequence satisfying the recurrence. The final constant is independent of the sequence and the order, so it introduces no new exponential base.

def OAI.RegularPointCoordinates.interiorConvolution line 25
Source documentation
The convolution with the two endpoint terms omitted.
```
def interiorConvolution (L : ℕ → ℝ) (m : ℕ) : ℝ :=
…
```
def OAI.RegularPointCoordinates.normalizedInteriorConvolution line 29
Source documentation
Normalized interior convolution from re:convolution-decay.
```
def normalizedInteriorConvolution (L : ℕ → ℝ) (m : ℕ) : ℝ :=
…
```
def OAI.RegularPointCoordinates.HasInverseMajorantRecurrence line 33
Source documentation
The positive-order recurrence after removing the exponential jet base.
```
def HasInverseMajorantRecurrence (L a : ℕ → ℝ) (A : ℝ) : Prop :=
…
```
theorem OAI.RegularPointCoordinates.interiorConvolution_nonneg line 37
theorem OAI.RegularPointCoordinates.normalizedInteriorConvolution_mul line 41

theorem OAI.RegularPointCoordinates.inverse_recurrence_step line 47

Source documentation

A bound at smaller orders controls the convolution in the recurrence.

theorem inverse_recurrence_step {L a : ℕ → ℝ} {A C : ℝ}
    (hL : ∀ m, 0 < L m) (hrec : HasInverseMajorantRecurrence L a A)
    {m : ℕ} (hm : 0 < m) (hprev : ∀ j < m, a j ≤ C * L j) :
    a m ≤ (A + Real.sqrt A * C * normalizedInteriorConvolution L m) * L m := by
…

Mentions: OAI.RegularPointCoordinates.HasInverseMajorantRecurrence, OAI.RegularPointCoordinates.normalizedInteriorConvolution

theorem OAI.RegularPointCoordinates.inverse_majorant_finite_prefix line 74

Source documentation

All orders below a finite cutoff have a common bound derived from the recurrence itself, uniform over every admissible sequence.

theorem inverse_majorant_finite_prefix {L : ℕ → ℝ} {A initial : ℝ}
    (hL : ∀ m, 0 < L m) (hinitial : 0 ≤ initial) (N : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ a : ℕ → ℝ,
      a 0 ≤ initial * L 0 → HasInverseMajorantRecurrence L a A →
      ∀ m < N, a m ≤ C * L m := by
…

Mentions: OAI.RegularPointCoordinates.HasInverseMajorantRecurrence

theorem OAI.RegularPointCoordinates.inverse_majorant_uniform line 102

Source documentation

Vanishing normalized convolution implies a uniform inverse majorant. The same constant works for every admissible sequence.

theorem inverse_majorant_uniform {L : ℕ → ℝ} {A initial : ℝ}
    (hL : ∀ m, 0 < L m) (hA : 0 ≤ A) (hinitial : 0 ≤ initial)
    (hdecay : Tendsto (normalizedInteriorConvolution L) atTop (𝓝 0)) :
    ∃ C : ℝ, initial ≤ C ∧ 2 * A ≤ C ∧ 0 ≤ C ∧
      ∀ a : ℕ → ℝ, a 0 ≤ initial * L 0 →
        HasInverseMajorantRecurrence L a A → ∀ m, a m ≤ C * L m := by
…

Mentions: OAI.RegularPointCoordinates.normalizedInteriorConvolution, OAI.RegularPointCoordinates.HasInverseMajorantRecurrence

theorem OAI.RegularPointCoordinates.inverse_coefficients_uniform_bound line 140

Source documentation

Specialization to the initial inverse norm √A used by the manuscript.

theorem inverse_coefficients_uniform_bound {L : ℕ → ℝ} {A : ℝ}
    (hL : ∀ m, 0 < L m) (hLzero : L 0 = 1) (hA : 1 ≤ A)
    (hdecay : Tendsto (normalizedInteriorConvolution L) atTop (𝓝 0)) :
    ∃ C : ℝ, Real.sqrt A ≤ C ∧ 2 * A ≤ C ∧
      ∀ a : ℕ → ℝ, a 0 ≤ Real.sqrt A →
        HasInverseMajorantRecurrence L a A → ∀ m, a m ≤ C * L m := by
…

Mentions: OAI.RegularPointCoordinates.normalizedInteriorConvolution, OAI.RegularPointCoordinates.HasInverseMajorantRecurrence