Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegularisedR3Final

(R3) of thm:regularised on a finite interval #

The statement of CKN.Leray.regularisedR3Final_core with every continuity hypothesis for the product topology on space-time, which is the parabolic topology.

source
@[instance_reducible]
def CKN.Leray.regularisedR3FinalNormedAddCommGroup :
NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group used for spatial and temporal regularity.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[instance_reducible]
    noncomputable def CKN.Leray.regularisedR3FinalNormedSpace :
    NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

    The product real normed space used for spatial and temporal derivatives.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      def CKN.Leray.regularisedR3FinalTopology :
      TopologicalSpace Foundation.Parabolic.ParabolicPoint

      The product topology on parabolic space-time points used in this weak identity.

      Equations
      Instances For
        source
        theorem CKN.Leray.regularised_R3_on_interval (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : ℝ) (hT : 0 < T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hL2Continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) (hDivFree : ∀ t ∈ Set.Icc 0 T, IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hMild : ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯ = realHeatOperator t ⋯ (realVectorL2OfCoordinateFunction (regUniformMollifiedInitial ρ ε hε a) ⋯) - regularizedMildStokesIntegral (regularizedMildTensorTrajectory ρ ε hε (regularisedIntervalMildCurve u T ⋯ hSlice)) t) (hUcontinuous : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDcontinuous : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDDcontinuous : ∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDtcontinuous : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hPcontinuous : ContinuousOn (regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDpcontinuous : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice y) i z) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hUjoint : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioc 0 T))) (hDdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioc 0 T), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, z.2)) z.1) (hPdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioc 0 T), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice (x, z.2)) z.1) :
        (∀ z ∈ spaceTimeSet Set.univ (Set.Ioo 0 T), ∀ (i : Fin 3), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z - ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) j z + ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε u y j * u y i) j z + spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice y) i z = 0) ∧ (∀ z ∈ spaceTimeSet Set.univ (Set.Ioo 0 T), ∀ (i : Fin 3), timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z - ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) j z + ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z + spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice y) i z = 0) ∧ ∀ (t : ℝ) (ht : t ∈ Set.Icc 0 T), (fun (x : Foundation.Parabolic.Vec3) => regularisedIntervalCanonicalPressure ρ ε hε u T ⋯ hSlice (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regularised_R3_on_interval._proof_1 (forcedPressureTensorLp (regularizedMildTensor ρ ε hε (realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) ⋯)))

        (R3) of thm:regularised on a finite interval: the same-velocity mild identity eq:reg-mild on [0, T] and the classical regularity on (0, T] give the regularized momentum equation in divergence and transport form on (0, T), and the pressure is the canonical Riesz pressure of each slice (R4).