The pairing of ∂_τ Θ_n against a test function, off the recentred axis #
The assembly CIV.dtPast_zoomTheta_pairing_bound_fixed of CIV.Zoom.RecedingDtPastPairingAssembly
with the offset A + R of eq:aniso:zoom:receding:equation only required to be positive on
the support; the assembly uses it only to stay off the recentred axis.
theorem
CIV.dtPast_zoomTheta_pairing_bound_fixed_of_pos
{h lam rc zc : ℝ}
(hlam : 0 < lam)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsol : IsClassicalSolutionOn u pr f unitCylinder)
(haxi : IsAxisymmetricOn u unitCylinder)
{K : Set (ℝ × ℝ)}
{τ : ℝ}
(hmem : ∀ y ∈ K, zoomPointRec lam h rc zc (y, τ) ∈ unitCylinder)
(hApos : ∀ y ∈ K, 0 < rc / lam + y.1)
(ψ : ℝ × ℝ → ℝ)
(hψU : tsupport ψ ⊆ interior K)
(B C_transport C_diffusion C_curvature C_swirl C_force : ℝ)
(T1 T2 T3 T4 T5 : ℝ × ℝ → ℝ)
(hT1_def :
T1 = 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, τ)))
(hT2_def :
T2 = 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, τ))
(hT3_def :
T3 = fun (y : ℝ × ℝ) =>
dr (fun (q : (ℝ × ℝ) × ℝ) => zoomTheta lam h rc zc u q) (y, τ) / (rc / lam + y.1) - zoomTheta lam h rc zc u (y, τ) / (rc / lam + y.1) ^ 2)
(hT4_def :
T4 = fun (y : ℝ × ℝ) => 1 / (rc / lam + y.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) (y, τ))
(hT5_def : T5 = fun (y : ℝ × ℝ) => lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc (y, τ)))
(hint1 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T1 y * ψ y) MeasureTheory.volume)
(hint2 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T2 y * ψ y) MeasureTheory.volume)
(hint3 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T3 y * ψ y) MeasureTheory.volume)
(hint4 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T4 y * ψ y) MeasureTheory.volume)
(hint5 : MeasureTheory.Integrable (fun (y : ℝ × ℝ) => T5 y * ψ y) MeasureTheory.volume)
(hbound1 : |∫ (y : ℝ × ℝ), T1 y * ψ y| ≤ C_transport * B)
(hbound2 : |∫ (y : ℝ × ℝ), T2 y * ψ y| ≤ C_diffusion * B)
(hbound3 : |∫ (y : ℝ × ℝ), T3 y * ψ y| ≤ C_curvature * B)
(hbound4 : |∫ (y : ℝ × ℝ), T4 y * ψ y| ≤ C_swirl * B)
(hbound5 : |∫ (y : ℝ × ℝ), T5 y * ψ y| ≤ C_force * B)
:
The five term pairings of eq:aniso:zoom:receding:equation (transport in divergence form,
diffusion, curvature, swirl source, force), each bounded against a test function ψ, bound
the pairing of ∂_τ Θ_n with ψ, through the divergence form zoomTheta_pde_divergenceForm
of the equation at every point of the support.