Documentation

LeanPool.CaffarelliKohnNirenberg.Leray.RegUniformMomentumIdentity

Reg Uniform Momentum Identity #

Supporting estimates for the Navier–Stokes development.

source
@[reducible, inline]
noncomputable abbrev CKN.Leray.regUniformParabolicTopologyMomentumIdentity :
TopologicalSpace Foundation.Parabolic.ParabolicPoint

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

Equations
Instances For
    source
    def CKN.Leray.regUniformParabolicHomeomorph :
    Foundation.Parabolic.ParabolicPoint ≃ₜ Foundation.Parabolic.Vec3 × ℝ

    The product homeomorphism identifying parabolic points with space-time pairs.

    Equations
    Instances For
      source
      @[instance_reducible]
      def CKN.Leray.instNormedAddCommGroupParabolicPoint_1 :
      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.instNormedSpaceRealParabolicPoint_1 :
        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.instTopologicalSpaceParabolicPoint :
          TopologicalSpace Foundation.Parabolic.ParabolicPoint

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

          Equations
          Instances For
            source
            theorem CKN.Leray.regUniform_momentum_identity (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (hSliceL2 : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hWeakDivFree : ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hUcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDcont : ∀ (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.Ioi 0))) (hDDcont : ∀ (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.Ioi 0))) (hDtcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hPcont : ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0))) (hDpcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hUcontDiff : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (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.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) (hEquation : ∀ (z : Foundation.Parabolic.ParabolicPoint), 0 < z.2 → ∀ (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) => p y) i z = 0) (φ : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) :
            ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, u z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * u z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z = 0

            The pointwise equation (R3), positive-time regularity (R1)–(R2), and weak solenoidality imply the regularized momentum identity in lem:reg-momentum.