Finite-family Hilbert energy chain rule

The high-order Sobolev energy is a finite sum of squared L² norms. Differentiating the Hilbert-space curves gives the time term in eq:lps-regularized-Hm-identity.

theorem ESS.lps_finite_l2_energy_chain {ι : Type u_1} (s : Finset ι) (F : ι → ℝ → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (G : ι → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) (t : ℝ) (hF : ∀ i ∈ s, HasDerivAt (F i) (G i) t) : HasDerivAt (fun (τ : ℝ) => ∑ i ∈ s, ‖F i τ‖ ^ 2) (2 * ∑ i ∈ s, inner ℝ (F i t) (G i)) t

The derivative of a finite sum of squared L² norms is twice the sum of the corresponding inner products (eq:lps-regularized-Hm-identity).

theorem ESS.lps_scalar_l2_inner_integral (F G : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : inner ℝ F G = ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑F x * ↑↑G x

The real L² inner product is the integral of the scalar product (eq:lps-regularized-Hm-identity).

theorem ESS.lps_scalar_l2_norm_sq_integral (F : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)) : ‖F‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑F x ^ 2

The squared real L² norm is the scalar square integral (eq:lps-regularized-Hm-identity).

theorem ESS.lps_scalar_l2_toLp_norm_sq_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

A square-integrable representative has the expected real L² norm formula (eq:lps-regularized-Hm-identity).

theorem ESS.lps_scalar_l2_toLp_inner_integral {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * g x

Representatives of two square-integrable fields compute their real L² inner product by integration (eq:lps-regularized-Hm-identity).