Reg Uniform Local Energy Flux

Supporting estimates for the Navier–Stokes development.

@[reducible, inline]

noncomputable abbrev CKN.Leray.regUniformParabolicTopologyLocalEnergyFlux : TopologicalSpace Foundation.Parabolic.ParabolicPoint

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

Equations

• CKN.Leray.regUniformParabolicTopologyLocalEnergyFlux = inferInstance

@[instance_reducible]

def CKN.Leray.regUniformLocalEnergyFluxNormedAddCommGroup : 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.

@[instance_reducible]

noncomputable def CKN.Leray.regUniformLocalEnergyFluxNormedSpace : 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.

@[instance_reducible]

def CKN.Leray.regUniformLocalEnergyFluxTopologicalSpace : TopologicalSpace Foundation.Parabolic.ParabolicPoint

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

Equations

• CKN.Leray.regUniformLocalEnergyFluxTopologicalSpace = instTopologicalSpaceProd

theorem CKN.Leray.regUniform_local_energy_flux_integral_zero (ρ : 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) (ψ : Foundation.Parabolic.ParabolicPoint → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) : have S := Set.univ ×ˢ Set.Ioi 0; have Ui := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => u z i; have D := fun (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z; have J := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => regUniformMollifiedVelocity ρ ε hε u z i; have Phi := fun (z : Foundation.Parabolic.Vec3 × ℝ) => ψ z; have H := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => Ui i z * Ui i z; have W := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => Ui i z * Phi z; have V := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => H i z * Phi z; have GradTest := fun (j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial Phi j z; have TimeFlux := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => V i z; have DiffFlux := fun (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => D i j z * W i z; have TestGradientFlux := fun (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => H i z * GradTest j z; have ConvFlux := fun (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => J j z * V i z; have PressureFlux := fun (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) => (fun (y : Foundation.Parabolic.Vec3 × ℝ) => p y) z * W i z; have FluxResidual := fun (z : Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, timePartialProd (TimeFlux i) z - 2 * ∑ i : Fin 3, ∑ j : Fin 3, spatialPartialProd (DiffFlux i j) j z + ∑ i : Fin 3, ∑ j : Fin 3, spatialPartialProd (TestGradientFlux i j) j z + ∑ i : Fin 3, ∑ j : Fin 3, spatialPartialProd (ConvFlux i j) j z + 2 * ∑ i : Fin 3, spatialPartialProd (PressureFlux i) i z; ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in S, FluxResidual z = 0

Compact support makes the integrated flux terms vanish in lem:reg-local-energy.