feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229)

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: RemyDegenne <remydegenne@gmail.com>

Author: RemyDegenne

src/measure_theory/integrable_on.lean

@@ -188,6 +188,17 @@ begin
   simpa only [set.univ_inter, measurable_set.univ, measure.restrict_apply] using hμs,
 end
 
+lemma integrable_on_Lp_of_measure_ne_top {E} [normed_group E] [measurable_space E] [borel_space E]
+  [second_countable_topology E] {p : ℝ≥0∞} {s : set α} (f : Lp E p μ) (hp : 1 ≤ p) (hμs : μ s ≠ ∞) :
+  integrable_on f s μ :=
+begin
+  refine mem_ℒp_one_iff_integrable.mp _,
+  have hμ_restrict_univ : (μ.restrict s) set.univ < ∞,
+    by simpa only [set.univ_inter, measurable_set.univ, measure.restrict_apply, lt_top_iff_ne_top],
+  haveI hμ_finite : finite_measure (μ.restrict s) := ⟨hμ_restrict_univ⟩,
+  exact ((Lp.mem_ℒp _).restrict s).mem_ℒp_of_exponent_le hp,
+end
+
 /-- We say that a function `f` is *integrable at filter* `l` if it is integrable on some
 set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.lift' powerset`. -/
 def integrable_at_filter (f : α → E) (l : filter α) (μ : measure α . volume_tac) :=

src/measure_theory/l2_space.lean

@@ -134,6 +134,61 @@ instance inner_product_space : inner_product_space 𝕜 (α →₂[μ] E) :=
 
 end inner_product_space
 
+section indicator_const_Lp
+
+variables [measurable_space 𝕜] [borel_space 𝕜] {s : set α}
+
+variables (𝕜)
+
+/-- The inner product in `L2` of the indicator of a set `indicator_const_Lp 2 hs hμs c` and `f` is
+equal to the integral of the inner product over `s`: `∫ x in s, ⟪c, f x⟫ ∂μ`. -/
+lemma inner_indicator_const_Lp_eq_set_integral_inner (f : Lp E 2 μ) (hs : measurable_set s) (c : E)
+  (hμs : μ s ≠ ∞) :
+  inner (indicator_const_Lp 2 hs hμs c) f = ∫ x in s, ⟪c, f x⟫ ∂μ :=
+begin
+  rw [inner_def, ← integral_add_compl hs (L2.integrable_inner _ f)],
+  have h_left : ∫ x in s, ⟪(indicator_const_Lp 2 hs hμs c) x, f x⟫ ∂μ = ∫ x in s, ⟪c, f x⟫ ∂μ,
+  { suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicator_const_Lp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫,
+      from set_integral_congr_ae hs h_ae_eq,
+    have h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → (indicator_const_Lp 2 hs hμs c x) = c,
+      from indicator_const_Lp_coe_fn_mem,
+    refine h_indicator.mono (λ x hx hxs, _),
+    congr,
+    exact hx hxs, },
+  have h_right : ∫ x in sᶜ, ⟪(indicator_const_Lp 2 hs hμs c) x, f x⟫ ∂μ = 0,
+  { suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicator_const_Lp 2 hs hμs c x, f x⟫ = 0,
+    { simp_rw ← set.mem_compl_iff at h_ae_eq,
+      suffices h_int_zero : ∫ x in sᶜ, inner (indicator_const_Lp 2 hs hμs c x) (f x) ∂μ
+        = ∫ x in sᶜ, (0 : 𝕜) ∂μ,
+      { rw h_int_zero,
+        simp, },
+      exact set_integral_congr_ae hs.compl h_ae_eq, },
+    have h_indicator : ∀ᵐ (x : α) ∂μ, x ∉ s → (indicator_const_Lp 2 hs hμs c x) = 0,
+      from indicator_const_Lp_coe_fn_nmem,
+    refine h_indicator.mono (λ x hx hxs, _),
+    rw hx hxs,
+    exact inner_zero_left, },
+  rw [h_left, h_right, add_zero],
+end
+
+/-- The inner product in `L2` of the indicator of a set `indicator_const_Lp 2 hs hμs c` and `f` is
+equal to the inner product of the constant `c` and the integral of `f` over `s`. -/
+lemma inner_indicator_const_Lp_eq_inner_set_integral [complete_space E] [normed_space ℝ E]
+  [is_scalar_tower ℝ 𝕜 E] (hs : measurable_set s) (hμs : μ s ≠ ∞) (c : E) (f : Lp E 2 μ) :
+  inner (indicator_const_Lp 2 hs hμs c) f = ⟪c, ∫ x in s, f x ∂μ⟫ :=
+by rw [← integral_inner (integrable_on_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs),
+    L2.inner_indicator_const_Lp_eq_set_integral_inner]
+
+variables {𝕜}
+
+/-- The inner product in `L2` of the indicator of a set `indicator_const_Lp 2 hs hμs (1 : ℝ)` and
+a real function `f` is equal to the integral of `f` over `s`. -/
+lemma inner_indicator_const_Lp_one (hs : measurable_set s) (hμs : μ s ≠ ∞) (f : Lp ℝ 2 μ) :
+  inner (indicator_const_Lp 2 hs hμs (1 : ℝ)) f = ∫ x in s, f x ∂μ :=
+by { rw L2.inner_indicator_const_Lp_eq_inner_set_integral ℝ hs hμs (1 : ℝ) f, simp, }
+
+end indicator_const_Lp
+
 end L2
 
 section inner_continuous

src/measure_theory/set_integral.lean

@@ -577,6 +577,24 @@ begin
     simp_rw [integrable_smul_const hc, hf, not_false_iff] }
 end
 
+section inner
+
+variables {E' : Type*} [inner_product_space 𝕜 E'] [measurable_space E'] [borel_space E']
+  [second_countable_topology E'] [complete_space E'] [normed_space ℝ E'] [is_scalar_tower ℝ 𝕜 E']
+
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 E' _ x y
+
+lemma integral_inner {f : α → E'} (hf : integrable f μ) (c : E') :
+  ∫ x, ⟪c, f x⟫ ∂μ = ⟪c, ∫ x, f x ∂μ⟫ :=
+((@inner_right 𝕜 E' _ _ c).restrict_scalars ℝ).integral_comp_comm hf
+
+lemma integral_eq_zero_of_forall_integral_inner_eq_zero (f : α → E') (hf : integrable f μ)
+  (hf_int : ∀ (c : E'), ∫ x, ⟪c, f x⟫ ∂μ = 0) :
+  ∫ x, f x ∂μ = 0 :=
+by { specialize hf_int (∫ x, f x ∂μ), rwa [integral_inner hf, inner_self_eq_zero] at hf_int }
+
+end inner
+
 end
 
 /-