Localized Equation Duhamel

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.Step3.localized_divergence_scalar_tested_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ spaceTimeTestFunction Ω I) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) (hφbox : tsupport φ ⊆ Ω' ×ˢ J) (i : Fin 3) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Set.univ Set.univ) : ∫ (z : Foundation.Parabolic.ParabolicPoint), localizedVelocity (have this := φ; this) u z i * (-timePartial ψ z - ∑ j : Fin 3, spatialSecondPartial ψ j j z) = (∫ (z : Foundation.Parabolic.ParabolicPoint), localizedDivergenceG φ u Du p f z i * ψ z) + ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint), localizedDivergenceH φ u p j z i * spatialPartial ψ j z

theorem CKN.Core.Step3.localized_divergence_source_data_hK_2 {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : (∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) → (∀ (j i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) → (∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => v z i) → have K := ((⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => v z i) ∪ ⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) ∪ ⋃ (j : Fin 3), ⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i; IsCompact K

theorem CKN.Core.Step3.localized_divergence_source_data_hKsupport_3 {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : have K := ((⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => v z i) ∪ ⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) ∪ ⋃ (j : Fin 3), ⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i; ∀ (hKx : IsCompact ((fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm z.1) '' K)) (hKt : IsCompact ((fun (z : Foundation.Parabolic.ParabolicPoint) => z.2) '' K)), have C := Classical.choose ⋯; (∀ x ∈ (fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm z.1) '' K, x ≤ C) → have a := Classical.choose ⋯; (∀ x ∈ (fun (z : Foundation.Parabolic.ParabolicPoint) => z.2) '' K, a ≤ x) → have b := Classical.choose ⋯; (∀ x ∈ (fun (z : Foundation.Parabolic.ParabolicPoint) => z.2) '' K, x ≤ b) → have r := max (C + 1) (|b - a| + 2); have t₀ := b + 1; b - a + 1 < r ^ 2 → ∀ z ∈ K, z.1 ∈ euclideanBall 0 r ∧ z.2 ∈ Set.Ioo (t₀ - r ^ 2) t₀

theorem CKN.Core.Step3.localized_divergence_source_data_hvi_10 {v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : HasCompactSupport v → ∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => v z i

theorem CKN.Core.Step3.localized_divergence_source_data_hrtime_11 {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} : have K := ((⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => v z i) ∪ ⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) ∪ ⋃ (j : Fin 3), ⋃ (i : Fin 3), tsupport fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i; ∀ (hKx : IsCompact ((fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm z.1) '' K)) (hKt : IsCompact ((fun (z : Foundation.Parabolic.ParabolicPoint) => z.2) '' K)), have C := Classical.choose ⋯; have a := Classical.choose ⋯; have b := Classical.choose ⋯; have r := max (C + 1) (|b - a| + 2); b - a + 1 < r ^ 2

theorem CKN.Core.Step3.localized_divergence_source_data_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ spaceTimeTestFunction Ω I) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) (hφbox : tsupport φ ⊆ Ω' ×ˢ J) : (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedVelocity (have this := φ; this) u z i) MeasureTheory.volume) ∧ (∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedDivergenceG φ u Du p f z i) MeasureTheory.volume) ∧ (∀ (j i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedDivergenceH φ u p j z i) MeasureTheory.volume) ∧ HasCompactSupport (localizedVelocity (have this := φ; this) u) ∧ (∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedDivergenceG φ u Du p f z i) ∧ ∀ (j i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedDivergenceH φ u p j z i

noncomputable def CKN.Core.Step3.duhamelSupportDataOfCompactSupport {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hv : HasCompactSupport v) (hg : ∀ (i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) (hh : ∀ (j i : Fin 3), HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) : DuhamelSupportData v g h

Construct common Duhamel support data from compact support of velocity and every source component.

Equations

• One or more equations did not get rendered due to their size.

def CKN.Core.Step3.parabolicHomeomorphReal' : Foundation.Parabolic.ParabolicPoint ≃ₜ Foundation.Parabolic.Vec3 × ℝ

Product-coordinate presentation of the parabolic point space used in weak-equation transport.

Equations

• CKN.Core.Step3.parabolicHomeomorphReal' = CKN.Foundation.Parabolic.parabolicHomeomorph

theorem CKN.Core.Step3.parabolic_potential_locallyIntegrable_of_compact_integrable {k g : Foundation.Parabolic.ParabolicPoint → ℝ} (hk : MeasureTheory.LocallyIntegrable k MeasureTheory.volume) (hkm : Measurable k) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) : MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.ParabolicPoint) => ∫ (y : Foundation.Parabolic.ParabolicPoint), k (HeatPotential.pointSub x y) * g y) MeasureTheory.volume