Bilinear forms with L∞ coefficients on L²

An essentially bounded field of continuous bilinear forms acts on two square-integrable functions by pointwise evaluation and integration. This file packages that operation as a continuous bilinear form using Mathlib's Hölder multiplication and Lᵖ pairing.

Main declarations

• TauCeti.lpBilinearForm: the continuous bilinear form associated to an L∞ field.
• TauCeti.lpBilinearForm_apply: its integral characterization.
• TauCeti.lpBilinearForm_congr_ae: invariance under a.e. equality of coefficient fields.

noncomputable def TauCeti.lpBilinearForm {X : Type u_1} {J : Type u_2} [MeasurableSpace X] [NormedAddCommGroup J] [NormedSpace ℝ J] (μ : MeasureTheory.Measure X) (B : ↥(MeasureTheory.Lp (J →L[ℝ] J →L[ℝ] ℝ) ⊤ μ)) : ↥(MeasureTheory.Lp J 2 μ) →L[ℝ] ↥(MeasureTheory.Lp J 2 μ) →L[ℝ] ℝ

The continuous bilinear form obtained by integrating an essentially bounded field of continuous bilinear forms against two square-integrable functions.

Equations

• TauCeti.lpBilinearForm μ B = ContinuousLinearMap.lpPairing μ 2 2 (ContinuousLinearMap.apply ℝ ℝ).flip ∘SL (ContinuousLinearMap.holderL μ ⊤ 2 2 (ContinuousLinearMap.apply ℝ (J →L[ℝ] ℝ)).flip) B

@[simp]

theorem TauCeti.lpBilinearForm_apply {X : Type u_1} {J : Type u_2} [MeasurableSpace X] [NormedAddCommGroup J] [NormedSpace ℝ J] (μ : MeasureTheory.Measure X) (B : ↥(MeasureTheory.Lp (J →L[ℝ] J →L[ℝ] ℝ) ⊤ μ)) (U V : ↥(MeasureTheory.Lp J 2 μ)) : ((lpBilinearForm μ B) U) V = ∫ (x : X), ((↑↑B x) (↑↑U x)) (↑↑V x) ∂μ

The L∞-coefficient bilinear form is the integral of its pointwise action.

theorem TauCeti.lpBilinearForm_congr_ae {X : Type u_1} {J : Type u_2} [MeasurableSpace X] [NormedAddCommGroup J] [NormedSpace ℝ J] {μ : MeasureTheory.Measure X} {B B' : ↥(MeasureTheory.Lp (J →L[ℝ] J →L[ℝ] ℝ) ⊤ μ)} (hB : ↑↑B =ᵐ[μ] ↑↑B') : lpBilinearForm μ B = lpBilinearForm μ B'

Replacing an L∞ coefficient field by an almost-everywhere equal field does not change the associated bilinear form.

theorem TauCeti.integrable_bilinear_apply_of_memLp {X : Type u_1} {J : Type u_2} [MeasurableSpace X] [NormedAddCommGroup J] [NormedSpace ℝ J] {μ : MeasureTheory.Measure X} {B : X → J →L[ℝ] J →L[ℝ] ℝ} (hB : MeasureTheory.MemLp B ⊤ μ) (U V : ↥(MeasureTheory.Lp J 2 μ)) : MeasureTheory.Integrable (fun (x : X) => ((B x) (↑↑U x)) (↑↑V x)) μ

Applying an L∞ field of bilinear forms to two L² functions gives an integrable scalar-valued function.