Quadratic data in affine parabolic coordinates

The finite local quadratic derivative data in thm:bu remains finite after the affine parabolic changes of variables used for time iteration.

theorem ESS.buAffinePoint_bounded_image (τ scale : ℝ) (hscale : 0 < scale) {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hK : Bornology.IsBounded K) : Bornology.IsBounded (buAffinePoint τ scale '' K)

Affine parabolic coordinates take bounded subsets of space-time to bounded subsets.

theorem ESS.bu_affine_l2_comp {E : Type u_1} [NormedAddCommGroup E] (τ scale : ℝ) (hscale : 0 < scale) (f : CKN.Foundation.Parabolic.ParabolicPoint → E) (hfloc : MeasureTheory.LocallyIntegrableOn f (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2))) MeasureTheory.volume) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖f z‖ₑ ^ 2 < ⊤) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) (hKsub : K ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)) (hKbounded : Bornology.IsBounded K) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, ‖f (buAffinePoint τ scale z)‖ₑ ^ 2 < ⊤

A finite quadratic integral on every bounded source subset transfers to every bounded subset of the normalized half-space cylinder.

theorem ESS.bu_affine_l2_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (τ scale c : ℝ) (hscale : 0 < scale) (hc : 0 ≤ c) (hc1 : c ≤ 1) (f : CKN.Foundation.Parabolic.ParabolicPoint → E) (hfloc : MeasureTheory.LocallyIntegrableOn f (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2))) MeasureTheory.volume) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2)), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖f z‖ₑ ^ 2 < ⊤) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) (hKsub : K ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)) (hKbounded : Bornology.IsBounded K) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, ‖c • f (buAffinePoint τ scale z)‖ₑ ^ 2 < ⊤

Finite local quadratic energy remains finite after affine composition and multiplication by a subunit scalar.

theorem ESS.bu_affine_derivative_l2 (τ scale : ℝ) (hτ : 0 ≤ τ) (hscale : 0 < scale) (hupper : τ + scale ^ 2 ≤ 1) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) : K ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) → Bornology.IsBounded K → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, ‖buAffineDw τ scale Dw z‖ₑ ^ 2 + ‖buAffineD2w τ scale D2w z‖ₑ ^ 2 + ‖buAffineDtw τ scale Dtw z‖ₑ ^ 2 < ⊤

The three quadratic derivative terms required by thm:bu remain finite on bounded subsets after an affine parabolic change of variables.