FinitePrefixEnvelope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Separating finitely many initial scales from a heat envelope

theorem OAI.RegularPointCoordinates.geometric_envelope_shift line 15

Source documentation

Shifting a geometric convolution leaves a finite initial contribution with the same geometric decay.

theorem geometric_envelope_shift (f : ℕ → ℝ) (β a : ℝ) (J i : ℕ) :
    β ^ (J + i) * a + ∑ j ∈ Finset.range (J + i + 1), β ^ (J + i - j) * f j =
      β ^ i * (β ^ J * a + ∑ j ∈ Finset.range J, β ^ (J - j) * f j) +
        ∑ j ∈ Finset.range (i + 1), β ^ (i - j) * f (J + j) := by
…

theorem OAI.RegularPointCoordinates.quadratic_le_opNorm line 38

theorem OAI.RegularPointCoordinates.finite_envelope_prefix_bound line 47

Source documentation

The initial contribution is bounded by a finite scalar, regardless of whether small-mass control holds at the omitted scales.

theorem finite_envelope_prefix_bound (N : ℕ → E →L[ℝ] E)
    {β : ℝ} (hβ : 0 ≤ β) (hβ1 : β ≤ 1) (J : ℕ) (v : E) :
    β ^ J * ‖v‖ ^ 2 + ∑ j ∈ Finset.range J, β ^ (J - j) * ⟪v, N j v⟫_ℝ ≤
      (1 + ∑ j ∈ Finset.range J, β ^ (J - j) * ‖N j‖) * ‖v‖ ^ 2 := by
…

theorem OAI.RegularPointCoordinates.shifted_heat_envelope_bound line 59

Source documentation

An eventual heat envelope has a finite background constant and the unchanged small-mass convolution after shifting the starting index.

theorem shifted_heat_envelope_bound (N F : ℕ → E →L[ℝ] E)
    {β : ℝ} (hβ : 0 ≤ β) (hβ1 : β ≤ 1)
    (henv : ∀ i v, ⟪v, F i v⟫_ℝ ≤ β ^ i * ‖v‖ ^ 2 +
      ∑ j ∈ Finset.range (i + 1), β ^ (i - j) * ⟪v, N j v⟫_ℝ)
    (J i : ℕ) (v : E) :
    ⟪v, F (J + i) v⟫_ℝ ≤
      (1 + ∑ j ∈ Finset.range J, β ^ (J - j) * ‖N j‖) * β ^ i * ‖v‖ ^ 2 +
        ∑ j ∈ Finset.range (i + 1), β ^ (i - j) * ⟪v, N (J + j) v⟫_ℝ := by
…