OAI/Geometry/RCD/Heat/EventualHeatCumulative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.eventual_heat_cumulative_comparison line 18

   Source documentation

   The cumulative comparison only needs its smallness and decrement bounds from some index onward. The earlier mass forms contribute a finite background; the absorption threshold is independent of that background.

   theorem eventual_heat_cumulative_comparison (Q : ℕ → E ≃L[ℝ] E)
       (N F : ℕ → E →L[ℝ] E) (J : ℕ)
       (hQ : ∀ i, (Q i : E →L[ℝ] E).IsPositive)
       (hN : ∀ i, (N i).IsPositive)
       {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C)
       (hstep : ∀ i, J ≤ i → ∀ v,
         ⟪v, Q i v⟫_ℝ ≤ (9 / 8 : ℝ) * ⟪v, Q (i + 1) v⟫_ℝ)
       (hdecrement : ∀ i, J ≤ i → ∀ v,
         let d := ⟪v, ((Q i : E →L[ℝ] E) - (Q (i + 1) : E →L[ℝ] E)) v⟫_ℝ
   …