OAI/Geometry/RCD/Heat/HeatControls.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The three actual heat estimates used by cumulative absorption

  1. structure OAI.RegularPointCoordinates.EventualHeatControls line 16

    Source documentation

    A common starting index, decrement constant and small-mass tolerance. These estimates are proved from the heat equation and splitting data.

    structure EventualHeatControls (Q : ℕ → E ≃L[ℝ] E)
    (N F : ℕ → E →L[ℝ] E) (J : ℕ) (ε C : ℝ) : Prop where
…