Quadratic data on affine time intervals #
Local quadratic data survives the change of variables from the physical
initial time interval to the shifted interval in lem:bu-small-time.
theorem
ESS.bu_affine_l2_comp_interval
{E : Type u_1}
[NormedAddCommGroup E]
(τ scale a b : ℝ)
(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 * a) (τ + scale ^ 2 * b)))
MeasureTheory.volume)
(hL2 :
∀
S ⊆
CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)),
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 a b))
(hKbounded : Bornology.IsBounded K)
:
A finite quadratic integral on bounded source subsets transfers to bounded subsets of a corresponding affine time interval.
theorem
ESS.bu_affine_l2_smul_interval
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(τ scale a b 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 * a) (τ + scale ^ 2 * b)))
MeasureTheory.volume)
(hL2 :
∀
S ⊆
CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b)),
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 a b))
(hKbounded : Bornology.IsBounded K)
:
Finite local quadratic energy remains finite after affine composition and multiplication by a subunit scalar.