Calculus facts for the regularized H¹ energy

Elementary real-analysis inputs to the differentiated energy identity of lem:lps-regularized-Hk-start and prop:lps-local-strong: differentiation of a scalar function from a paired increment, L² continuity of products, and the sup-norm bound of a convolution by L² norms.

theorem ESS.LPS.lps_hasDerivAt_of_pair_increment {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ℝ → ℝ} {R Θ : ι → ℝ → E} {a : ℝ} (hR : ∀ (i : ι), ContinuousAt (R i) a) (hΘ : ∀ (i : ι), ContinuousAt (Θ i) a) (hInc : ∀ᶠ (c : ℝ) in nhds a, IntervalIntegrable (fun (r : ℝ) => ∑ i : ι, inner ℝ (R i r) (Θ i a + Θ i c)) MeasureTheory.volume a c ∧ φ c - φ a = ∫ (r : ℝ) in a..c, ∑ i : ι, inner ℝ (R i r) (Θ i a + Θ i c)) : HasDerivAt φ (2 * ∑ i : ι, inner ℝ (R i a) (Θ i a)) a

A scalar function whose increments over [a,c] are the integrals of the pairing of a path R, continuous at a, against Θ a + Θ c, with Θ continuous at a, has derivative 2 ⟪R a, Θ a⟫ at a (prop:lps-local-strong).

theorem ESS.LPS.lps_lp_norm_sq_eq_integral {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp f hf‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2

The squared L² norm of the class of a square-integrable function is its integral of squares.

theorem ESS.LPS.lps_lp_dist_sq_eq_integral {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : ‖MeasureTheory.MemLp.toLp f hf - MeasureTheory.MemLp.toLp g hg‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), (f x - g x) ^ 2

The squared distance of two L² classes is the integral of the squared difference of representatives.

theorem ESS.LPS.lps_continuousAt_toLp_of_sq_tendsto {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hmem : ∀ (r : ℝ), MeasureTheory.MemLp (f r) 2 MeasureTheory.volume) {a : ℝ} (h : Filter.Tendsto (fun (r : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (f r x - f a x) ^ 2) (nhds a) (nhds 0)) : ContinuousAt (fun (r : ℝ) => MeasureTheory.MemLp.toLp (f r) ⋯) a

Convergence of squared L² distances is continuity of the induced L² path.

theorem ESS.LPS.lps_sq_tendsto_of_continuousAt_toLp {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hmem : ∀ (r : ℝ), MeasureTheory.MemLp (f r) 2 MeasureTheory.volume) {a : ℝ} (h : ContinuousAt (fun (r : ℝ) => MeasureTheory.MemLp.toLp (f r) ⋯) a) : Filter.Tendsto (fun (r : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (f r x - f a x) ^ 2) (nhds a) (nhds 0)

Continuity of an L² path gives convergence of the squared L² distances of its representatives.

theorem ESS.LPS.lps_sq_tendsto_mul {A B : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {a M : ℝ} {ν : ℝ → ℝ} (hBa : MeasureTheory.MemLp (B a) 2 MeasureTheory.volume) (hB : ∀ᶠ (r : ℝ) in nhds a, MeasureTheory.MemLp (B r) 2 MeasureTheory.volume) (hBt : Filter.Tendsto (fun (r : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (B r x - B a x) ^ 2) (nhds a) (nhds 0)) (hM : ∀ᶠ (r : ℝ) in nhds a, ∀ (x : CKN.Foundation.Parabolic.Vec3), |A r x| ≤ M) (hν : Filter.Tendsto ν (nhds a) (nhds 0)) (hAν : ∀ᶠ (r : ℝ) in nhds a, ∀ (x : CKN.Foundation.Parabolic.Vec3), |A r x - A a x| ≤ ν r) : Filter.Tendsto (fun (r : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (A r x * B r x - A a x * B a x) ^ 2) (nhds a) (nhds 0)

The product of a uniformly bounded, uniformly convergent factor with an L²-convergent factor converges in L².

theorem ESS.LPS.lps_convolution_diff_abs_le {κ f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : MeasureTheory.MemLp κ 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) : |MeasureTheory.convolution κ f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x - MeasureTheory.convolution κ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x| ≤ √(∫ (t : CKN.Foundation.Parabolic.Vec3), κ t ^ 2) * √(∫ (t : CKN.Foundation.Parabolic.Vec3), (f t - g t) ^ 2)

The pointwise difference of two convolutions with a fixed L² kernel is bounded by the kernel's L² norm times the L² distance of the two arguments.

noncomputable def ESS.LPS.lpsPath (f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ) (hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume) (s : ℝ) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The L² class of a time-dependent function, with time clamped to [0, ∞).

Equations

• ESS.LPS.lpsPath f hf s = MeasureTheory.MemLp.toLp (f (max s 0)) ⋯

theorem ESS.LPS.lps_lpsPath_apply {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume} {r : ℝ} (hr : 0 ≤ r) : lpsPath f hf r = MeasureTheory.MemLp.toLp (f r) ⋯

On nonnegative times the clamped L² path is the class of the function itself.

theorem ESS.LPS.lps_lpsPath_coeFn {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume} {r : ℝ} (hr : 0 ≤ r) : ↑↑(lpsPath f hf r) =ᵐ[MeasureTheory.volume] f r

On nonnegative times the clamped L² path is represented by the function itself.

theorem ESS.LPS.lps_continuousAt_lpsPath_of_path {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume} {a : ℝ} {F : ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)} (ha : 0 < a) (hF : ContinuousAt F a) (hae : ∀ᶠ (r : ℝ) in nhds a, ↑↑(F r) =ᵐ[MeasureTheory.volume] f r) : ContinuousAt (lpsPath f hf) a

A clamped L² path is continuous at a positive time where it agrees near that time with an L²-continuous path.

theorem ESS.LPS.lps_lpsPath_coeFn' {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume} (r : ℝ) : ↑↑(lpsPath f hf r) =ᵐ[MeasureTheory.volume] f (max r 0)

Every value of the clamped L² path is represented by the function at the clamped time.

theorem ESS.LPS.lps_lpsPath_finsetSum {ι : Type u_1} (s : Finset ι) {f : ι → ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (i : ι) (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (f i t) 2 MeasureTheory.volume} {g : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hg : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (g t) 2 MeasureTheory.volume} (hsum : ∀ (t : ℝ) (x : CKN.Foundation.Parabolic.Vec3), g t x = ∑ i ∈ s, f i t x) (r : ℝ) : lpsPath g hg r = ∑ i ∈ s, lpsPath (f i) ⋯ r

The clamped L² path of a finite sum of functions is the sum of the paths.

theorem ESS.LPS.lps_lpsPath_sub {f g h : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (f t) 2 MeasureTheory.volume} {hg : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (g t) 2 MeasureTheory.volume} {hh : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (h t) 2 MeasureTheory.volume} (hsub : ∀ (t : ℝ) (x : CKN.Foundation.Parabolic.Vec3), h t x = f t x - g t x) (r : ℝ) : lpsPath h hh r = lpsPath f hf r - lpsPath g hg r

The clamped L² path of a difference is the difference of the paths.

theorem ESS.LPS.lps_lpsPath_neg {f h : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (f t) 2 MeasureTheory.volume} {hh : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (h t) 2 MeasureTheory.volume} (hneg : ∀ (t : ℝ) (x : CKN.Foundation.Parabolic.Vec3), h t x = -f t x) (r : ℝ) : lpsPath h hh r = -lpsPath f hf r

The clamped L² path of a negative is the negative of the path.

theorem ESS.LPS.lps_inner_lpsPath {f g : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (f t) 2 MeasureTheory.volume} {hg : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (g t) 2 MeasureTheory.volume} (r c : ℝ) : inner ℝ (lpsPath f hf r) (lpsPath g hg c) = ∫ (x : CKN.Foundation.Parabolic.Vec3), f (max r 0) x * g (max c 0) x

The inner product of two clamped L² paths is the integral of the product of the functions at the clamped times.

theorem ESS.LPS.lps_sq_tendsto_of_continuousAt_lpsPath {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume} {a : ℝ} (ha : 0 < a) (h : ContinuousAt (lpsPath f hf) a) : Filter.Tendsto (fun (r : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (f r x - f a x) ^ 2) (nhds a) (nhds 0)

Continuity of a clamped L² path at a positive time gives convergence of the squared L² distances of the underlying functions.

theorem ESS.LPS.lps_continuousAt_lpsPath_of_sq_tendsto {f : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} {hf : ∀ (s : ℝ), 0 ≤ s → MeasureTheory.MemLp (f s) 2 MeasureTheory.volume} {a : ℝ} (ha : 0 < a) (h : Filter.Tendsto (fun (r : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (f r x - f a x) ^ 2) (nhds a) (nhds 0)) : ContinuousAt (lpsPath f hf) a

Convergence of squared L² distances at a positive time gives continuity of the clamped L² path.