Spatial weak derivatives across the gluing time #
A spatial weak-derivative identity on a slab extends, without any boundary
term, to test fields that do not vanish at the ends of the slab, by a time
cutoff and dominated convergence. Consequently spatial weak derivatives of two
adjacent slabs glue (lem:lps-continuation).
theorem
ESS.lps_cutoff_right_integral_tendsto
{ν : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)}
{A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(b : ℝ)
(hA : MeasureTheory.Integrable A ν)
(hlt : ∀ᵐ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂ν, q.2 < b)
:
Filter.Tendsto (fun (ε : ℝ) => ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), lpsCutoffRight b ε q.2 * A q ∂ν)
(nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), A q ∂ν))
Cutting off near the right end of a slab and letting the cutoff width tend to zero recovers the integral.
theorem
ESS.lps_cutoff_left_integral_tendsto
{ν : MeasureTheory.Measure (CKN.Foundation.Parabolic.Vec3 × ℝ)}
{A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(a : ℝ)
(hA : MeasureTheory.Integrable A ν)
(hgt : ∀ᵐ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂ν, a < q.2)
:
Filter.Tendsto (fun (ε : ℝ) => ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), lpsCutoffLeft a ε q.2 * A q ∂ν)
(nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), A q ∂ν))
The left-end version of lps_cutoff_right_integral_tendsto.
theorem
ESS.lps_spatial_weak_extend_right
{a b c : ℝ}
{F G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{j : Fin 3}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hw :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), G z * φ z)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), G z * φ z
A spatial weak-derivative identity on a slab extends to test fields on a larger slab, when restricted to the smaller one.
theorem
ESS.lps_spatial_weak_extend_left
{a b c : ℝ}
{F G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{j : Fin 3}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c))))
(hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c))))
(hw :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo b c),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), G z * φ z)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), G z * φ z
The left-end version of lps_spatial_weak_extend_right.
theorem
ESS.lps_spatial_weak_glue
{a b c : ℝ}
(hab : a < b)
(hbc : b < c)
{F₁ F₂ F G₁ G₂ G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{j : Fin 3}
(hF₁ : MeasureTheory.MemLp F₁ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hG₁ : MeasureTheory.MemLp G₁ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
(hF₂ : MeasureTheory.MemLp F₂ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c))))
(hG₂ : MeasureTheory.MemLp G₂ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c))))
(hw₁ :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F₁ z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), G₁ z * φ z)
(hw₂ :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo b c),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), F₂ z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), G₂ z * φ z)
(hF : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ b → F z = F₁ z)
(hF' : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), b < z.2 → F z = F₂ z)
(hG : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ b → G z = G₁ z)
(hG' : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), b < z.2 → G z = G₂ z)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c))
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), G z * φ z
Spatial weak derivatives of two adjacent slabs glue.