HeatBaseBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Starting the cumulative argument at any positive heat metric

theorem OAI.RegularPointCoordinates.positive_equiv_inverse_comparison line 18

Source documentation

Every positive invertible heat metric has finite two-sided inverse comparison constants, even before choosing a normalized initial frame.

theorem positive_equiv_inverse_comparison (Q : E ≃L[ℝ] E)
    (hQ : (Q : E →L[ℝ] E).IsPositive) (v : E) :
    ⟪v, Q.symm v⟫_ℝ ≤ ‖(Q.symm : E →L[ℝ] E)‖ * ‖v‖ ^ 2 ∧
      ‖v‖ ^ 2 ≤ ‖(Q : E →L[ℝ] E)‖ * ⟪v, Q.symm v⟫_ℝ := by
…

theorem OAI.RegularPointCoordinates.inverse_norm_sq_of_slow_growth_coercive line 42

Source documentation

Slow adjacent growth propagates any finite initial coercivity constant to the squared norm of all inverse metrics.

theorem inverse_norm_sq_of_slow_growth_coercive (Q : ℕ → E ≃L[ℝ] E)
    {B : ℝ} (hB : 0 ≤ B)
    (hstep : ∀ i v, ⟪v, Q i v⟫_ℝ ≤ (9 / 8 : ℝ) * ⟪v, Q (i + 1) v⟫_ℝ)
    (hbase : ∀ v, ‖v‖ ^ 2 ≤ B * ⟪v, Q 0 v⟫_ℝ) (i : ℕ) (v : E) :
    ‖(Q i).symm v‖ ^ 2 ≤ B ^ 2 * (81 / 64 : ℝ) ^ i * ‖v‖ ^ 2 := by
…