Uniform slice bounds from continuity #
prop:lps-smoothing: the slices of an L²-continuous family of order M on a compact time
interval have uniformly bounded H^M energy, and the same bound holds for almost every slice
of the space-time family that the curves represent.
theorem
ESS.lps_integral_sq_eq_toReal_sq
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2 = (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal ^ 2
The square integral of a square-integrable real function is the square of its L² norm.
theorem
ESS.lps_l2Norm_continuousOn
{S : Set ℝ}
{f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ∀ t ∈ S, MeasureTheory.MemLp (f t) 2 MeasureTheory.volume)
(hcont :
∀ t ∈ S,
Filter.Tendsto
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f s x - f t x) 2 MeasureTheory.volume)
(nhdsWithin t S) (nhds 0))
:
ContinuousOn (fun (t : ℝ) => (MeasureTheory.eLpNorm (f t) 2 MeasureTheory.volume).toReal) S
The L² norm of an L²-continuous curve is continuous.
theorem
ESS.lps_ladder_slice_bound
{a b : ℝ}
{M : ℕ}
{Z : Fin 3 → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ}
{DD : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hfam : ∀ (i : Fin 3), ∀ t ∈ Set.Icc a b, CKN.IsSobolevFamilyOn M Set.univ (Z i t []) (Z i t))
(hcont :
∀ (i : Fin 3) (α : List (Fin 3)),
α.length ≤ M →
∀ t ∈ Set.Icc a b,
Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z i s α - Z i t α) 2 MeasureTheory.volume)
(nhdsWithin t (Set.Icc a b)) (nhds 0))
(hae :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (i : Fin 3) (α : List (Fin 3)),
α.length ≤ M → Z i t α =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => DD i α (x, t))
:
Uniform H^M slice bounds for a family of order M whose slices are L²-continuous on a
compact interval [a, b] and represent, for almost every time, the derivatives of a space-time
family (prop:lps-smoothing).