The correction between raw and centred cutoff sources

The raw divergence source and the centred cutoff source differ by cutoff and spatial-mean terms. Linearity transports this explicit correction to the completed spatial Riesz operators.

noncomputable def CKN.Core.Step4.centredRawSourceCorrection (B : Set Foundation.Parabolic.Vec3) (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (c : Foundation.Parabolic.Vec3) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : ℝ

The cutoff and mean correction relative to a raw source on B.

Equations

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

theorem CKN.Core.Step4.centred_source_sub_force_eq_raw_add_correction (B : Set Foundation.Parabolic.Vec3) (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (c : Foundation.Parabolic.Vec3) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : pressureDivergenceCutoffSourceCentredTensor η dη u Du c x i - η x * f x i = B.indicator (fun (y : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du y i k * u y k - f y i) x + centredRawSourceCorrection B η dη u f Du c i x

The centred source minus its near-force source equals the raw source plus the explicit cutoff and mean correction.

theorem CKN.Core.Step4.gradient_riesz_add_ae (j i : Fin 3) {a b : Foundation.Parabolic.Vec3 → ℝ} (ha : MeasureTheory.MemLp a (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hb : MeasureTheory.MemLp b (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (a + b) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ a + Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ b

The completed gradient Riesz operator is additive on its actual domain.

theorem CKN.Core.Step4.gradient_riesz_sub_ae (j i : Fin 3) {a b : Foundation.Parabolic.Vec3 → ℝ} (ha : MeasureTheory.MemLp a (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hb : MeasureTheory.MemLp b (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (a - b) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ a - Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ b

Subtraction is respected almost everywhere on the completed operator domain.

theorem CKN.Core.Step4.centredRawSourceCorrection_memLp (B : Set Foundation.Parabolic.Vec3) (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (c : Foundation.Parabolic.Vec3) (j : Fin 3) (hV : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hF : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => η x * f x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hG : MeasureTheory.MemLp (B.indicator fun (x : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du x j k * u x k - f x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : MeasureTheory.MemLp (centredRawSourceCorrection B η dη u f Du c j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The correction belongs to the operator domain whenever the two original sources and the localized force do.

theorem CKN.Core.Step4.centred_riesz_eq_raw_add_correction_ae (B : Set Foundation.Parabolic.Vec3) (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (c : Foundation.Parabolic.Vec3) (j i : Fin 3) (hV : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hF : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => η x * f x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hG : MeasureTheory.MemLp (B.indicator fun (x : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du x j k * u x k - f x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : (Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c x j - η x * f x j) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (B.indicator fun (x : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du x j k * u x k - f x j) + Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (centredRawSourceCorrection B η dη u f Du c j)

The exact Riesz identity retains the correction term; the raw and centred fields are not silently substituted for each other.

theorem CKN.Core.Step4.signed_centred_riesz_eq_raw_corrected_ae (B A : Set Foundation.Parabolic.Vec3) (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3) (c : Foundation.Parabolic.Vec3) (i : Fin 3) (hV : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hF : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => η x * f x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hG : ∀ (j : Fin 3), MeasureTheory.MemLp (B.indicator fun (x : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du x j k * u x k - f x j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : (fun (x : Foundation.Parabolic.Vec3) => -∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c y j) x + ∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => η y * f y j) x) =ᵐ[MeasureTheory.volume.restrict A] fun (x : Foundation.Parabolic.Vec3) => -∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (B.indicator fun (y : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du y j k * u y k - f y j) x - ∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (centredRawSourceCorrection B η dη u f Du c j) x

The signed centred Riesz contribution is exactly the signed raw contribution minus the correction, on every measurable or nonmeasurable spatial restriction.