UniformCumulativeConstants.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Cumulative constants uniform over a family of heat poles

theorem OAI.RegularPointCoordinates.exists_uniform_heat_cumulative_constants line 19

Source documentation

A uniform bound on the finite background and initial metric gives one set of cumulative constants for every heat pole in a neighborhood. The geometric absorption threshold is unchanged by the background.

theorem exists_uniform_heat_cumulative_constants
    {b T ε C : ℝ} (hb : 1 ≤ b) (hT : 0 < T) (hε : 0 ≤ ε) (hC : 0 ≤ C)
    (habsorb : 2 * C * (2 * geometricIntervalConstant ((3 / 4 : ℝ) * (9 / 8))) * ε ≤ 1 / 2) :
    ∃ A B D : ℝ, 0 < A ∧ 0 < B ∧ 0 < D ∧
    ∀ (Q : ℕ → E ≃L[ℝ] E) (N F : ℕ → E →L[ℝ] E) (J : ℕ),
    (∀ i, (Q i : E →L[ℝ] E).IsPositive) →
    (∀ i, (N i).IsPositive) →
    (∀ i, J ≤ i → ∀ v, ⟪v, Q i v⟫_ℝ ≤ (9 / 8 : ℝ) * ⟪v, Q (i + 1) v⟫_ℝ) →
    (∀ i, J ≤ i → ∀ v,
      let d := ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ
…

Mentions: OAI.RegularPointCoordinates.geometricIntervalConstant