Scalar Hilbert pairings on space-time slabs

The scalar real L² pairing is an integral on any measurable carrier. Strong L² convergence consequently implies convergence against every fixed L² test field.

theorem ESS.lps_scalar_lp_inner_integral_generic {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = ∫ (z : α), f z * g z ∂μ

The real scalar L² pairing equals the integral of the product on any measurable carrier (prop:lps-smoothing).

theorem ESS.lps_scalar_lp_inner_left_integral_generic {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (F : ↥(MeasureTheory.Lp ℝ 2 μ)) {g : α → ℝ} (hg : MeasureTheory.MemLp g 2 μ) : inner ℝ F (MeasureTheory.MemLp.toLp g hg) = ∫ (z : α), ↑↑F z * g z ∂μ

A scalar L² class pairs with a square-integrable representative by integrating its chosen measurable representative (prop:lps-smoothing).

theorem ESS.lps_scalar_lp_pairing_tendsto_of_strong {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {fseq : ℕ → α → ℝ} {f w : α → ℝ} (hfseq : ∀ (n : ℕ), MeasureTheory.MemLp (fseq n) 2 μ) (hf : MeasureTheory.MemLp f 2 μ) (hw : MeasureTheory.MemLp w 2 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fseq n - f) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : α), fseq n z * w z ∂μ) Filter.atTop (nhds (∫ (z : α), f z * w z ∂μ))

Strong scalar L² convergence gives convergence of all fixed L² pairings (prop:lps-smoothing).