Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedBesselLocalRealBall

Closed real trajectory ball for the complete Sobolev fixed point #

The complete Sobolev local mild map will be contracted on the closed ball of trajectories with real physical L² realization.

source
def CKN.Leray.regularisedBesselLocalRealBall (k : ℕ) (T R : ℝ) :
Set C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)

Continuous complete H²ᵏ trajectories inside the local norm ball whose physical L² fields are real.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CKN.Leray.regularisedBesselLocalRealBall_isClosed (k : ℕ) (T R : ℝ) :
    IsClosed (regularisedBesselLocalRealBall k T R)

    The real complete Sobolev trajectory ball is closed.

    source
    theorem CKN.Leray.regularisedBesselLocalRealBall_zero (k : ℕ) (T R : ℝ) (hR : 0 ≤ R) :
    0 ∈ regularisedBesselLocalRealBall k T R

    The zero trajectory lies in every real local ball with nonnegative radius.