RescaledHeatEnvelope.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Normalizing a finite initial contribution without changing absorption

theorem OAI.RegularPointCoordinates.rescaled_heat_envelope line 17

Source documentation

Dividing both mass forms by the finite background constant restores the normalized envelope used in the cumulative theorem.

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

theorem OAI.RegularPointCoordinates.rescaled_heat_decrements line 40

Source documentation

The paired rescaling of the envelope and its mass forms keeps both decrement inequalities, at the common constant b*C.

theorem rescaled_heat_decrements (N F D : E →L[ℝ] E)
    {b C : ℝ} (hb : 1 ≤ b) (hC : 0 ≤ C)
    (hD : ∀ v, 0 ≤ ⟪v, D v⟫_ℝ)
    (hlower : ∀ v, ⟪v, N v⟫_ℝ ≤ C * ⟪v, D v⟫_ℝ)
    (hupper : ∀ v, ⟪v, D v⟫_ℝ ≤ C * ⟪v, F v⟫_ℝ) (v : E) :
    ⟪v, (b⁻¹ • N) v⟫_ℝ ≤ (b * C) * ⟪v, D v⟫_ℝ ∧
      ⟪v, D v⟫_ℝ ≤ (b * C) * ⟪v, (b⁻¹ • F) v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.rescaled_absorption_identity line 59
Source documentation
The smallness constant scales reciprocally to the decrement constant, so the absorption condition is unchanged by the finite background.
```
theorem rescaled_absorption_identity {b : ℝ} (hb : 0 < b) (C W ε : ℝ) :
    2 * (b * C) * W * (b⁻¹ * ε) = 2 * C * W * ε := by
…
```