HeatCutoffEnergy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Local energy inequality for the actual heat flow

The cutoff operator acts on both L² and the actual Sobolev space. Its self-adjointness identifies the time derivative with the admissible square-cutoff test. No bound on the initial heat datum is used.

theorem OAI.RegularPointCoordinates.heat_cutoff_norm_hasDerivAt line 22
theorem OAI.RegularPointCoordinates.cutoff_L2_norm_sq line 43

theorem OAI.RegularPointCoordinates.heat_cutoff_energy_differential line 57

Source documentation

The differential local energy inequality, with the cutoff error kept as a localized integral.

theorem heat_cutoff_energy_differential (f : Lp ℝ 2 μ) (η : SobolevSpace μ hQ)
    {χ : X → ℝ} {L B A : ℝ≥0} (hχ : LipschitzWith L χ)
    (hs : HasCompactSupport χ) (hb : ∀ x, |χ x| ≤ B) (hn : ∀ x, 0 ≤ χ x)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
    (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A)
    (t : ℝ) (ht : 0 < t) :
    let V := boundedMultiplier μ χ hχ.continuous.measurable B hb
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope, OAI.RegularPointCoordinates.boundedMultiplier