Pointwise time derivatives of the smooth slice representatives

lem:lps-Bochner-joint-smooth: if the weak pairings of the slices with spatial tests are differentiable in time with continuous derivative given by the next slice, the pointwise values of the smooth representatives are differentiable in time with the corresponding derivative.

theorem ESS.lps_hasDerivWithinAt_Icc_of_integral {a b : ℝ} (hab : a < b) {f g : ℝ → ℝ} (hg : ContinuousOn g (Set.Icc a b)) (hid : ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, s ≤ t → f t - f s = ∫ (τ : ℝ) in s..t, g τ) (t : ℝ) : t ∈ Set.Icc a b → HasDerivWithinAt f (g t) (Set.Icc a b) t

If a real function is a primitive of a function continuous on [a,b] on all subintervals, it is differentiable within [a,b] with that derivative (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_abs_integral_pairing_le (f g : CKN.Foundation.Parabolic.Vec3 → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : |∫ (x : CKN.Foundation.Parabolic.Vec3), f x * g x| ≤ √(∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2) * √(∫ (x : CKN.Foundation.Parabolic.Vec3), g x ^ 2)

The absolute value of an L² pairing is at most the product of the norms (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_pairing_continuousOn {a b : ℝ} {Z : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hmem : ∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (Z t) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z s - Z t) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) : ContinuousOn (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z s x * ψ x) (Set.Icc a b)

A curve of L² fields that is L²-continuous has continuous spatial pairings with any L² test (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_pairing_integral_identity {a b : ℝ} {Z Z' : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hmem' : ∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (Z' t) 2 MeasureTheory.volume) (hcont' : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z' s - Z' t) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hψ : MeasureTheory.MemLp ψ 2 MeasureTheory.volume) (hderiv : ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z s x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z' t x * ψ x) (Set.Icc a b) t) (s : ℝ) : s ∈ Set.Icc a b → ∀ t ∈ Set.Icc a b, s ≤ t → (∫ (x : CKN.Foundation.Parabolic.Vec3), Z t x * ψ x) - ∫ (x : CKN.Foundation.Parabolic.Vec3), Z s x * ψ x = ∫ (τ : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), Z' τ x * ψ x

Fundamental theorem of calculus for the spatial pairings of a slice curve (lem:lps-Bochner-joint-smooth).

noncomputable def ESS.lpsBump (r : ℝ) (hr : 0 < r) : ContDiffBump 0

The bump function of outer radius r used to build approximate identities.

Equations

• ESS.lpsBump r hr = { rIn := r / 2, rOut := r, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def ESS.lpsBumpTest (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : CKN.Foundation.Parabolic.Vec3 → ℝ

The normalized bump of radius r centred at x₀, as a test function.

Equations

• ESS.lpsBumpTest x₀ r hr y = (ESS.lpsBump r hr).normed MeasureTheory.volume (x₀ - y)

theorem ESS.lpsBumpTest_contDiff (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : ContDiff ℝ (↑⊤) (lpsBumpTest x₀ r hr)

theorem ESS.lpsBumpTest_hasCompactSupport (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) : HasCompactSupport (lpsBumpTest x₀ r hr)

theorem ESS.lpsBumpTest_pairing (x₀ : CKN.Foundation.Parabolic.Vec3) (r : ℝ) (hr : 0 < r) (h : CKN.Foundation.Parabolic.Vec3 → ℝ) : ∫ (y : CKN.Foundation.Parabolic.Vec3), h y * lpsBumpTest x₀ r hr y = MeasureTheory.convolution ((lpsBump r hr).normed MeasureTheory.volume) h (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x₀

Pairing with the normalized bump at x₀ is convolution with the bump at x₀.

theorem ESS.lps_pointwise_time_identity {a b : ℝ} {Z Z' B B' : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hBs : ∀ t ∈ Set.Icc a b, ContDiff ℝ (↑⊤) (B t) ∧ B t =ᵐ[MeasureTheory.volume] Z t) (hBs' : ∀ t ∈ Set.Icc a b, ContDiff ℝ (↑⊤) (B' t) ∧ B' t =ᵐ[MeasureTheory.volume] Z' t) (hmem' : ∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (Z' t) 2 MeasureTheory.volume) (hcont' : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z' s - Z' t) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) (hderiv : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z s x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z' t x * ψ x) (Set.Icc a b) t) (hW' : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => B' z.2 z.1) (Set.univ ×ˢ Set.Icc a b)) (x₀ : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : s ∈ Set.Icc a b → ∀ t ∈ Set.Icc a b, s ≤ t → B t x₀ - B s x₀ = ∫ (τ : ℝ) in s..t, B' τ x₀

The pointwise values of the smooth slice representatives satisfy the integral form of the time equation (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_pointwise_time_hasDerivWithinAt {a b : ℝ} (hab : a < b) {Z Z' B B' : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hBs : ∀ t ∈ Set.Icc a b, ContDiff ℝ (↑⊤) (B t) ∧ B t =ᵐ[MeasureTheory.volume] Z t) (hBs' : ∀ t ∈ Set.Icc a b, ContDiff ℝ (↑⊤) (B' t) ∧ B' t =ᵐ[MeasureTheory.volume] Z' t) (hmem' : ∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (Z' t) 2 MeasureTheory.volume) (hcont' : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z' s - Z' t) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) (hderiv : ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z s x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z' t x * ψ x) (Set.Icc a b) t) (hW' : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => B' z.2 z.1) (Set.univ ×ˢ Set.Icc a b)) (x₀ : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : t ∈ Set.Icc a b → HasDerivWithinAt (fun (s : ℝ) => B s x₀) (B' t x₀) (Set.Icc a b) t

The pointwise values of the smooth slice representatives are differentiable in time within [a,b], with derivative the value of the next slice representative (lem:lps-Bochner-joint-smooth).