The transport/divergence term T1

theorem CIV.continuous_mul_of_tsupport_subset_pairing {U : Set (ℝ × ℝ)} (hU : IsOpen U) {a b : ℝ × ℝ → ℝ} (ha : ContinuousOn a U) (hb : Continuous b) (hbU : tsupport b ⊆ U) : Continuous fun (y : ℝ × ℝ) => a y * b y

The product of a function continuous on an open set with a continuous function whose support closes inside that set is continuous on the whole plane.

theorem CIV.integrable_transportTerm_mul_zoomTheta {lam h rc zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => -(dr (fun (q : (ℝ × ℝ) × ℝ) => zoomVRec lam h rc zc u q * zoomTheta lam h rc zc u q) (y, τ) + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomWRec lam h rc zc u q * zoomTheta lam h rc zc u q) (y, τ)) * ψ y) MeasureTheory.volume

Integrability of the transport/divergence term of zoomTheta_pde_divergenceForm against a test function ψ supported in the interior of a compact set K, at a fixed zoom scale. Public restatement of the continuity argument CIV.RecedingTransportPairingBound's private proof already carries, exposed for CIV.dtPast_zoomTheta_pairing_bound_fixed's hint1.

The diffusion term T2

theorem CIV.integrable_diffusionTerm_mul_zoomTheta {lam h rc zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => (dr (dr fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) + (lam ^ (2 * h)) ^ 2 * dz (dz fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ)) * ψ y) MeasureTheory.volume

Integrability of the diffusion term of zoomTheta_pde_divergenceForm against a test function ψ supported in the interior of a compact set K, at a fixed zoom scale. Public restatement of the continuity argument CIV.RecedingDiffusionPairingBound's private proof already carries, exposed for CIV.dtPast_zoomTheta_pairing_bound_fixed's hint2.

The curvature term T3

theorem CIV.integrable_curvatureTerm_mul_zoomTheta {lam h rc zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (hApos : ∀ y ∈ K, 0 < rc / lam + y.1) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => (dr (zoomTheta lam h rc zc u) (y, τ) / (rc / lam + y.1) - zoomTheta lam h rc zc u (y, τ) / (rc / lam + y.1) ^ 2) * ψ y) MeasureTheory.volume

Integrability of the curvature term of zoomTheta_pde_divergenceForm against a test function ψ supported in the interior of a compact set K, at a fixed zoom scale. Public restatement of the continuity argument CIV.RecedingCurvaturePairingBound's private proof already carries, exposed for CIV.dtPast_zoomTheta_pairing_bound_fixed's hint3.

The swirl term T4

theorem CIV.integrable_swirlTerm_mul_zoomTheta {lam h rc zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) (hApos : ∀ y ∈ K, 0 < rc / lam + y.1) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => 1 / (rc / lam + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) (y, τ) * ψ y) MeasureTheory.volume

Integrability of the swirl term of zoomTheta_pde_divergenceForm against a test function ψ supported in the interior of a compact set K, at a fixed zoom scale. Public restatement of the continuity argument CIV.RecedingSwirlPairingBound's private proof already carries, exposed for CIV.dtPast_zoomTheta_pairing_bound_fixed's hint4.

The force term T5

theorem CIV.integrable_forceTerm_mul_zoomTheta {lam h rc zc : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) {K : Set (ℝ × ℝ)} {τ : ℝ} (hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder) {ψ : ℝ × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ interior K) : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc (y, τ)) * ψ y) MeasureTheory.volume

Integrability of the force term of zoomTheta_pde_divergenceForm against a test function ψ supported in the interior of a compact set K, at a fixed zoom scale. Uses the force's own smoothness (from IsClassicalSolutionOn) composed with the smooth recentred zoom point, exposed for CIV.dtPast_zoomTheta_pairing_bound_fixed's hint5.