The localized weak time identity for a compact spatial weight

@[instance_reducible]

def CKN.Leray.regTailsWeakIdentityNormedAddCommGroup : 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.regTailsWeakIdentityNormedSpace : 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.regTailsWeakIdentityTopologicalSpace : TopologicalSpace Foundation.Parabolic.ParabolicPoint

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

Equations

• CKN.Leray.regTailsWeakIdentityTopologicalSpace = instTopologicalSpaceProd

theorem CKN.Leray.regTailsWeakIdentityOpensMeasurableSpace : OpensMeasurableSpace Foundation.Parabolic.ParabolicPoint

theorem CKN.Leray.regTailsWeakIdentityProductVolumeIsAddHaarMeasure : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.Leray.regTails_localized_weak_time_identity (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (J : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hLE : ∀ ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), 2 * ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), spatialGradientSq u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) z * ψ z = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * (timePartial ψ z + ∑ i : Fin 3, spatialSecondPartial ψ i i z) + ∑ i : Fin 3, (Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * J z i + 2 * p z * u z i) * spatialPartial ψ i z) (hUcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (hDcont : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (Set.univ ×ˢ Set.Ioi 0)) (hPcont : ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2)) (Set.univ ×ˢ Set.Ioi 0)) (hJcont : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (hUdiff : ∀ (i : Fin 3), ContDiffOn ℝ 1 (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (z.1, z.2) i) (Set.univ ×ˢ Set.Ioi 0)) (q : Foundation.Parabolic.Vec3 → ℝ) (hq : ContDiff ℝ (↑⊤) q) (hqc : HasCompactSupport q) (η : ℝ → ℝ) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηI : tsupport η ⊆ Set.Ioi 0) : ∫ (t : ℝ), regTailsEnergyWeight u q t * deriv η t = -∫ (t : ℝ), (∫ (x : Foundation.Parabolic.Vec3), regTailsLocalizedSource u (fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) p J q (x, t)) * η t

The compactly localized energy identity gives a distributional time derivative for every smooth compact spatial weight.