Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedGlobalMild

Global mild evolution of the regularized equation #

The zero-force instance of the forced construction gives a global mild trajectory. Its restriction agrees with the local mild solution by unrestricted mild uniqueness.

source
theorem CKN.Leray.forcedHeatLeray_zero (τ : ℝ) (hτ : 0 ≤ τ) :
forcedHeatLeray τ hτ 0 = 0

The Leray-projected heat operator sends the zero field to zero.

source
theorem CKN.Leray.forcedForceDuhamel_zero (t : ℝ) :
forcedForceDuhamel (fun (x : ℝ) => 0) t = 0

The zero forcing term has no Duhamel contribution.

source
noncomputable def CKN.Leray.regularizedGlobalMildCurve (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) :
ℝ → ↥RealVectorL2

The zero-force specialization of the forced solution curve.

Equations
Instances For
    source
    theorem CKN.Leray.regularizedGlobalMildCurve_continuous (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) :
    Continuous (regularizedGlobalMildCurve ρ ε hε b hb)

    The zero-force global mild curve is continuous in spatial L².

    source
    theorem CKN.Leray.regularizedGlobalMildCurve_mildJData (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) (t : ℝ) (ht : 0 ≤ t) :
    RegularizedMildJData (regularizedGlobalMildCurve ρ ε hε b hb t)

    Every nonnegative-time state of the zero-force mild curve belongs to the divergence-free L² space.

    source
    theorem CKN.Leray.regularizedGlobalMildCurve_zero (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) :
    regularizedGlobalMildCurve ρ ε hε b hb 0 = b

    The global zero-force mild curve starts at the prescribed L² state.

    source
    theorem CKN.Leray.regularizedGlobalMildCurve_norm_le_initial (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) (t : ℝ) (ht : 0 ≤ t) :
    ‖regularizedGlobalMildCurve ρ ε hε b hb t‖ ≤ ‖b‖

    The zero-force global mild curve has nonincreasing L² norm.

    source
    theorem CKN.Leray.regularizedGlobalMildCurve_mild (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) (t : ℝ) (ht : 0 ≤ t) :
    regularizedGlobalMildCurve ρ ε hε b hb t = realHeatOperator t ht b - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε (regularizedGlobalMildCurve ρ ε hε b hb)) t

    The global zero-force curve satisfies the same nonlinear mild equation at every nonnegative time.

    source
    theorem CKN.Leray.regularizedGlobalMildCurve_isTrajectory (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : ↥RealVectorL2) (hb : RegularizedMildJData b) (T : ℝ) :
    IsRegularizedMildTrajectory ρ ε hε b T { toFun := fun (t : ↑(RegularizedMildTimeInterval T)) => regularizedGlobalMildCurve ρ ε hε b hb ↑t, continuous_toFun := ⋯ }

    The global zero-force curve restricts to a mild trajectory on every finite nonnegative interval.