Pairings under parabolic rescaling

Spatial test functions and their momentum pairings transform covariantly under the affine maps used in prop:blowup-limit.

theorem ESS.blowup_limit_integral_comp_affine (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : ∫ (x : CKN.Foundation.Parabolic.Vec3), f (x₀ + r • x) = r⁻¹ ^ 3 * ∫ (y : CKN.Foundation.Parabolic.Vec3), f y

Change variables in an integral under a spatial translation and positive dilation.

noncomputable def ESS.blowupLimitPullbackTest (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3) : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3

A vector test pulled back along translation and parabolic spatial rescaling.

Equations

• ESS.blowupLimitPullbackTest x₀ r w y = CKN.weakContL3OfLp (w (r⁻¹ • (y - x₀)))

theorem ESS.blowup_limit_rescaled_trace_pairing_source_formula (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))))) (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (hW : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x)) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hformula : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4) → ∀ (s t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), (∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v t) y).ofLp i * ψ y i) - ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v s) y).ofLp i * ψ y i = ∫ (τ : ℝ) in ↑s..↑t, ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3, ∑ j : Fin 3, u (y, τ) i * u (y, τ) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y - ∑ i : Fin 3, ∑ j : Fin 3, Du (y, τ) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y + p (y, τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) i y) {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3} {C : Set CKN.Foundation.Parabolic.Vec3} (hw : ContDiff ℝ (↑⊤) w) (hwsupport : tsupport w ⊆ C) (hC : IsCompact C) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (himage : (fun (x : CKN.Foundation.Parabolic.Vec3) => x₀ + r • x) '' C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (a b : ℝ) (htime : ∀ t ∈ Set.Icc a b, t₀ + r ^ 2 * t ∈ Set.Icc (-(3 / 4) ^ 2) 0) (s t : ↑(Set.Icc a b)) : (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitTraceRescaling W x₀ t₀ r (x, ↑t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitTraceRescaling W x₀ t₀ r (x, ↑s) i * (w x).ofLp i = r⁻¹ ^ 2 * ∫ (τ : ℝ) in t₀ + r ^ 2 * ↑s..t₀ + r ^ 2 * ↑t, ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3, ∑ j : Fin 3, u (y, τ) i * u (y, τ) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPullbackTest x₀ r w z i) j y - ∑ i : Fin 3, ∑ j : Fin 3, Du (y, τ) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPullbackTest x₀ r w z i) j y + p (y, τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPullbackTest x₀ r w z i) i y

A compactly supported rescaled test pairs with the all-time source trace by the source momentum formula, with the exact parabolic time factor.

theorem ESS.blowup_limit_rescaled_trace_pairing_source_time_formula (v : ↑(Set.Icc (-(3 / 4) ^ 2) 0) → ↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))))) (W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3) (hW : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))] fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x)) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hformula : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4) → ∀ (s t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), (∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v t) y).ofLp i * ψ y i) - ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v s) y).ofLp i * ψ y i = ∫ (τ : ℝ) in ↑s..↑t, ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3, ∑ j : Fin 3, u (y, τ) i * u (y, τ) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y - ∑ i : Fin 3, ∑ j : Fin 3, Du (y, τ) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y + p (y, τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) i y) {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3} {C : Set CKN.Foundation.Parabolic.Vec3} (hw : ContDiff ℝ (↑⊤) w) (hwsupport : tsupport w ⊆ C) (hC : IsCompact C) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) (himage : (fun (x : CKN.Foundation.Parabolic.Vec3) => x₀ + r • x) '' C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (a b : ℝ) (htime : ∀ t ∈ Set.Icc a b, t₀ + r ^ 2 * t ∈ Set.Icc (-(3 / 4) ^ 2) 0) (s t : ↑(Set.Icc a b)) : (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitTraceRescaling W x₀ t₀ r (x, ↑t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, blowupLimitTraceRescaling W x₀ t₀ r (x, ↑s) i * (w x).ofLp i = ∫ (τ : ℝ) in ↑s..↑t, ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3, ∑ j : Fin 3, u (y, t₀ + r ^ 2 * τ) i * u (y, t₀ + r ^ 2 * τ) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPullbackTest x₀ r w z i) j y - ∑ i : Fin 3, ∑ j : Fin 3, Du (y, t₀ + r ^ 2 * τ) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPullbackTest x₀ r w z i) j y + p (y, t₀ + r ^ 2 * τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => blowupLimitPullbackTest x₀ r w z i) i y

The source formula remains an interval-integral identity after parabolic time reparameterization, including either endpoint of the closed interval.