Calculus of space-time Sobolev families on slabs

prop:lps-smoothing: elementary operations on L²(I; H^m(ℝ³)) families used by the regularity ladder: lowering the order, restricting to a smaller time interval, differentiating once (the shifted family), and finite sums, together with the restriction of the distributional heat equation to a smaller time interval.

theorem ESS.lps_l2Family_toSpaceTime {m : ℕ} {I : Set ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : CKN.IsL2SobolevFamilyOn m Set.univ I z D) : IsSpaceTimeFamily m (Set.univ ×ˢ I) D

An L²(I; H^m) family is a space-time derivative family on the slab.

theorem ESS.lps_spaceTimeFamily_toL2 {m : ℕ} {I : Set ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeFamily m (Set.univ ×ˢ I) D) (hz : D [] =ᵐ[MeasureTheory.volume.restrict (Set.univ ×ˢ I)] z) : CKN.IsL2SobolevFamilyOn m Set.univ I z D

A space-time derivative family on a slab whose zeroth member represents z is an L²(I; H^m) family of z.

theorem ESS.lps_l2Family_of_le {m m' : ℕ} {I : Set ℝ} {z : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : CKN.IsL2SobolevFamilyOn m Set.univ I z D) (hm : m' ≤ m) : CKN.IsL2SobolevFamilyOn m' Set.univ I z D

An L²(I; H^m) family is an L²(I; H^{m'}) family for every m' ≤ m.

theorem ESS.lps_l2Family_mono_interval {m : ℕ} {I J : Set ℝ} (hI : MeasurableSet I) (hJI : J ⊆ I) {z : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : CKN.IsL2SobolevFamilyOn m Set.univ I z D) : CKN.IsL2SobolevFamilyOn m Set.univ J z D

An L²(I; H^m) family restricts to every measurable subinterval J ⊆ I.

theorem ESS.lps_l2Family_shift {m : ℕ} {I : Set ℝ} {z g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : CKN.IsL2SobolevFamilyOn (m + 1) Set.univ I z D) (j : Fin 3) (hg : D [j] =ᵐ[MeasureTheory.volume.restrict (Set.univ ×ˢ I)] g) : CKN.IsL2SobolevFamilyOn m Set.univ I g fun (γ : List (Fin 3)) => D (j :: γ)

Differentiating once: the words of an L²(I; H^{m+1}) family that start with j form an L²(I; H^m) family of any representative g of D [j].

theorem ESS.lps_l2Family_sum {m : ℕ} {I : Set ℝ} {f : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : Fin 3 → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : ∀ (j : Fin 3), CKN.IsL2SobolevFamilyOn m Set.univ I (f j) (D j)) : CKN.IsL2SobolevFamilyOn m Set.univ I (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, f j z) fun (α : List (Fin 3)) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, D j α z

Finite sums of L²(I; H^m) families over the three coordinates.

theorem ESS.lps_heat_mono_interval {I J : Set ℝ} (hI : MeasurableSet I) (hJI : J ⊆ I) {z G : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : CKN.IsHeatSolutionOn Set.univ I z G) : CKN.IsHeatSolutionOn Set.univ J z G

The distributional heat equation restricts to a measurable subinterval.

theorem ESS.lps_sum_sobolevWords_two (φ : List (Fin 3) → ℝ) : ∑ α ∈ CKN.sobolevWords 2, φ α = φ [] + ∑ j : Fin 3, φ [j] + ∑ j : Fin 3, ∑ k : Fin 3, φ [j, k]

The sum over the words of length at most two, written out.