OAI/Geometry/RCD/Heat/HeatUpperIncrement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual upper heat decrement from finite Gaussian mass shells

  1. theorem OAI.RegularPointCoordinates.dyadic_heat_increment_upper_bound line 25

    Source documentation

    Integrate the proved upper derivative on a dyadic time block. The hypothesis is a bound on actual heat mass, not a decrement assumption.

    theorem dyadic_heat_increment_upper_bound (hρ : 0 < ρ) (hρr : ρ < r) (hκ : 0 ≤ κ)
    {s E η lambda : ℝ} (hs : 0 < s) (hlambda0 : 0 ≤ lambda)
    (hlambda : 2 * κ * (L : ℝ) ^ 2 + η ≤ lambda)
    (herror : ∀ t ∈ Icc (s ^ 2 / 4) (s ^ 2), ‖harmonicHeatError μ hQ (k := ker) G χ t p‖ ≤ η)
…

    Mentions: OAI.RegularPointCoordinates.harmonicHeatError