Documentation

LeanPool.EscauriazaSereginSverak.Linear.BUShortCutoffOperator

Heat operator of the short-time cutoff field #

The specified weak heat vector separates into the scaled equation and the first and second derivatives of the smooth cutoff in lem:bu-small-time.

source
noncomputable def ESS.buCutHeatError (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
CKN.Foundation.Parabolic.Vec3

The cutoff derivative terms in the weak heat equation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ESS.buCutHeat_eq (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :
    ucWeakHeatVector (buCutD2 κ v Dv D2v) (buCutDt κ v Dtv) z = buCutScalar κ z • ucWeakHeatVector D2v Dtv z + buCutHeatError κ v Dv z

    The weak heat vector of the cutoff field is the scalar cutoff times the original weak heat vector plus the cutoff derivative error.