[Merged by Bors] - feat(measure_theory/l2_space): L2 is an inner product space

docs/undergrad.yaml

@@ -431,7 +431,8 @@ Topology:
     orthogonal projection onto closed vector subspaces: 'orthogonal_projection_fn'
     dual space: 'normed_space.dual.normed_space'
     Riesz representation theorem: 'inner_product_space.to_dual'
-    $l^2$ and $L^2$ cases:
+    inner product spaces $l^2$ and $L^2$: 'measure_theory.L2.inner_product_space'
+    their completeness: 'measure_theory.Lp.complete_space'
     Hilbert (orthonormal) bases (in the separable case): 'exists_is_orthonormal_dense_span'
     Hilbert basis of trigonometric polynomials:
     Hilbert bases of orthogonal polynomials:

src/algebra/group_power/basic.lean

@@ -706,6 +706,14 @@ end
 @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
 by simp [pow, monoid.pow]
 
+lemma sub_pow_two {R} [comm_ring R] (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 :=
+by rw [sub_eq_add_neg, add_pow_two, neg_square, mul_neg_eq_neg_mul_symm, ← sub_eq_add_neg]
+
+/-- Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings. -/
+lemma two_mul_le_add_pow_two {R} [linear_ordered_comm_ring R] (a b : R) :
+  2 * a * b ≤ a ^ 2 + b ^ 2 :=
+sub_nonneg.mp ((sub_add_eq_add_sub _ _ _).subst ((sub_pow_two a b).subst (pow_two_nonneg _)))
+
 lemma of_add_nsmul [add_monoid A] (x : A) (n : ℕ) :
   multiplicative.of_add (n •ℕ x) = (multiplicative.of_add x)^n := rfl
 

src/algebra/ordered_field.lean

@@ -540,6 +540,14 @@ by { rw [div_lt_iff (@zero_lt_two α _ _)], exact lt_mul_of_one_lt_right h one_l
 
 lemma half_lt_self : 0 < a → a / 2 < a := div_two_lt_of_pos
 
+lemma half_le_self (ha_nonneg : 0 ≤ a) : a / 2 ≤ a :=
+begin
+  by_cases h0 : a = 0,
+  { simp [h0], },
+  { rw ← ne.def at h0,
+    exact (half_lt_self (lt_of_le_of_ne ha_nonneg h0.symm)).le, },
+end
+
 lemma one_half_lt_one : (1 / 2 : α) < 1 := half_lt_self zero_lt_one
 
 lemma add_sub_div_two_lt (h : a < b) : a + (b - a) / 2 < b :=

src/analysis/normed_space/inner_product.lean

@@ -1740,6 +1740,19 @@ lemma measurable.inner [measurable_space α] [measurable_space E] [opens_measura
   measurable (λ t, ⟪f t, g t⟫) :=
 continuous.measurable2 continuous_inner hf hg
 
+lemma ae_measurable.inner [measurable_space α] [measurable_space E] [opens_measurable_space E]
+  [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜]
+  {μ : measure_theory.measure α} {f g : α → E} (hf : ae_measurable f μ) (hg : ae_measurable g μ) :
+  ae_measurable (λ x, ⟪f x, g x⟫) μ :=
+begin
+  refine ⟨λ x, ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, _⟩,
+  refine hf.ae_eq_mk.mp (hg.ae_eq_mk.mono (λ x hxg hxf, _)),
+  dsimp only,
+  congr,
+  { exact hxf, },
+  { exact hxg, },
+end
+
 variables [topological_space α] {f g : α → E} {x : α} {s : set α}
 
 include 𝕜

src/measure_theory/bochner_integration.lean

@@ -68,6 +68,12 @@ The Bochner integral is defined following these steps:
 
 4. `tendsto_integral_of_dominated_convergence` : the Lebesgue dominated convergence theorem
 
+5. (In the file `set_integral`) integration commutes with continuous linear maps.
+
+  * `continuous_linear_map.integral_comp_comm`
+  * `linear_isometry.integral_comp_comm`
+
+
 ## Notes
 
 Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that

src/measure_theory/l1_space.lean

@@ -515,6 +515,11 @@ lemma mem_ℒp.integrable [borel_space β] {q : ℝ≥0∞} (hq1 : 1 ≤ q) {f :
   (hfq : mem_ℒp f q μ) : integrable f μ :=
 mem_ℒp_one_iff_integrable.mp (hfq.mem_ℒp_of_exponent_le hq1)
 
+lemma lipschitz_with.integrable_comp_iff_of_antilipschitz [complete_space β] [borel_space β]
+  [borel_space γ] {K K'} {f : α → β} {g : β → γ} (hg : lipschitz_with K g)
+  (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
+  integrable (g ∘ f) μ ↔ integrable f μ :=
+by simp [← mem_ℒp_one_iff_integrable, hg.mem_ℒp_comp_iff_of_antilipschitz hg' g0]
 
 section pos_part
 /-! ### Lemmas used for defining the positive part of a `L¹` function -/

src/measure_theory/l2_space.lean

@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2021 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+import analysis.normed_space.inner_product
+import measure_theory.set_integral
+
+/-! # `L^2` space
+
+If `E` is an inner product space over `𝕜` (`ℝ` or `ℂ`), then `Lp E 2 μ` (defined in `lp_space.lean`)
+is also an inner product space, with inner product defined as `inner f g = ∫ a, ⟪f a, g a⟫ ∂μ`.
+
+### Main results
+
+* `mem_L1_inner` : for `f` and `g` in `Lp E 2 μ`, the pointwise inner product `λ x, ⟪f x, g x⟫`
+  belongs to `Lp 𝕜 1 μ`.
+* `integrable_inner` : for `f` and `g` in `Lp E 2 μ`, the pointwise inner product `λ x, ⟪f x, g x⟫`
+  is integrable.
+* `L2.inner_product_space` : `Lp E 2 μ` is an inner product space.
+
+### Notation
+
+* `α →₂[μ] E` : the type `Lp E 2 μ`.
+
+-/
+
+noncomputable theory
+open topological_space measure_theory measure_theory.Lp
+open_locale nnreal ennreal
+
+notation α ` →₂[`:25 μ `] ` E := measure_theory.Lp E 2 μ
+
+namespace measure_theory
+namespace L2
+
+variables {α E F 𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space α] {μ : measure α}
+  [measurable_space E] [inner_product_space 𝕜 E] [borel_space E] [second_countable_topology E]
+  [normed_group F] [measurable_space F] [borel_space F] [second_countable_topology F]
+
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
+
+lemma snorm_rpow_two_norm_lt_top (f : Lp F 2 μ) : snorm (λ x, ∥f x∥ ^ (2 : ℝ)) 1 μ < ∞ :=
+begin
+  have h_two : ennreal.of_real (2 : ℝ) = 2, by simp [zero_le_one],
+  rw [snorm_norm_rpow f zero_lt_two, one_mul, h_two],
+  exact ennreal.rpow_lt_top_of_nonneg zero_le_two (Lp.snorm_ne_top f),
+end
+
+lemma snorm_inner_lt_top (f g : Lp E 2 μ) : snorm (λ (x : α), ⟪f x, g x⟫) 1 μ < ∞ :=
+begin
+  have h : ∀ x, is_R_or_C.abs ⟪f x, g x⟫ ≤ ∥f x∥ * ∥g x∥, from λ x, abs_inner_le_norm _ _,
+  have h' : ∀ x, is_R_or_C.abs ⟪f x, g x⟫ ≤ is_R_or_C.abs (∥f x∥^2 + ∥g x∥^2),
+  { refine λ x, le_trans (h x) _,
+    rw [is_R_or_C.abs_to_real, abs_eq_self.mpr],
+    swap, { exact add_nonneg (by simp) (by simp), },
+    refine le_trans _ (half_le_self (add_nonneg (pow_two_nonneg _) (pow_two_nonneg _))),
+    refine (le_div_iff (@zero_lt_two ℝ _ _)).mpr ((le_of_eq _).trans (two_mul_le_add_pow_two _ _)),
+    ring, },
+  simp_rw [← is_R_or_C.norm_eq_abs, ← real.rpow_nat_cast] at h',
+  refine (snorm_mono_ae (ae_of_all _ h')).trans_lt ((snorm_add_le _ _ le_rfl).trans_lt _),
+  { exact (Lp.ae_measurable f).norm.rpow_const, },
+  { exact (Lp.ae_measurable g).norm.rpow_const, },
+  simp only [nat.cast_bit0, ennreal.add_lt_top, nat.cast_one],
+  exact ⟨snorm_rpow_two_norm_lt_top f, snorm_rpow_two_norm_lt_top g⟩,
+end
+
+section inner_product_space
+
+variables [measurable_space 𝕜] [borel_space 𝕜]
+
+include 𝕜
+
+instance : has_inner 𝕜 (Lp E 2 μ) := ⟨λ f g, ∫ a, ⟪f a, g a⟫ ∂μ⟩
+
+lemma inner_def (f g : Lp E 2 μ) : inner f g = ∫ a : α, ⟪f a, g a⟫ ∂μ := rfl
+
+lemma integral_inner_eq_sq_snorm (f : Lp E 2 μ) :
+  ∫ a, ⟪f a, f a⟫ ∂μ = ennreal.to_real ∫⁻ a, (nnnorm (f a) : ℝ≥0∞) ^ (2:ℝ) ∂μ :=
+begin
+  simp_rw inner_self_eq_norm_sq_to_K,
+  norm_cast,
+  rw integral_eq_lintegral_of_nonneg_ae,
+  swap, { exact filter.eventually_of_forall (λ x, pow_two_nonneg _), },
+  swap, { exact (Lp.ae_measurable f).norm.pow, },
+  congr,
+  ext1 x,
+  have h_two : (2 : ℝ) = ((2 : ℕ) : ℝ), by simp,
+  rw [← real.rpow_nat_cast _ 2, ← h_two,
+    ← ennreal.of_real_rpow_of_nonneg (norm_nonneg _) zero_le_two, of_real_norm_eq_coe_nnnorm],
+  norm_cast,
+end
+
+private lemma norm_sq_eq_inner' (f : Lp E 2 μ) : ∥f∥ ^ 2 = is_R_or_C.re (inner f f : 𝕜) :=
+begin
+  have h_two : (2 : ℝ≥0∞).to_real = 2 := by simp,
+  rw [inner_def, integral_inner_eq_sq_snorm, norm_def, ← ennreal.to_real_pow, is_R_or_C.of_real_re,
+    ennreal.to_real_eq_to_real (ennreal.pow_lt_top (Lp.snorm_lt_top f) 2) _],
+  { rw [←ennreal.rpow_nat_cast, snorm_eq_snorm' ennreal.two_ne_zero ennreal.two_ne_top, snorm',
+      ← ennreal.rpow_mul, one_div, h_two],
+    simp, },
+  { refine lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top zero_lt_two _,
+    rw [← h_two, ← snorm_eq_snorm' ennreal.two_ne_zero ennreal.two_ne_top],
+    exact Lp.snorm_lt_top f, },
+end
+
+lemma mem_L1_inner (f g : Lp E 2 μ) :
+  ae_eq_fun.mk (λ x, ⟪f x, g x⟫) ((Lp.ae_measurable f).inner (Lp.ae_measurable g)) ∈ Lp 𝕜 1 μ :=
+by { simp_rw [mem_Lp_iff_snorm_lt_top, snorm_ae_eq_fun], exact snorm_inner_lt_top f g, }
+
+lemma integrable_inner (f g : Lp E 2 μ) : integrable (λ x : α, ⟪f x, g x⟫) μ :=
+(integrable_congr (ae_eq_fun.coe_fn_mk (λ x, ⟪f x, g x⟫)
+    ((Lp.ae_measurable f).inner (Lp.ae_measurable g)))).mp
+  (ae_eq_fun.integrable_iff_mem_L1.mpr (mem_L1_inner f g))
+
+private lemma add_left' (f f' g : Lp E 2 μ) : (inner (f + f') g : 𝕜) = inner f g + inner f' g :=
+begin
+  simp_rw [inner_def, ← integral_add (integrable_inner f g) (integrable_inner f' g),
+    ←inner_add_left],
+  refine integral_congr_ae ((coe_fn_add f f').mono (λ x hx, _)),
+  congr,
+  rwa pi.add_apply at hx,
+end
+
+private lemma smul_left' (f g : Lp E 2 μ) (r : 𝕜) :
+  inner (r • f) g = is_R_or_C.conj r * inner f g :=
+begin
+  rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul],
+  refine integral_congr_ae ((coe_fn_smul r f).mono (λ x hx, _)),
+  rw [smul_eq_mul, ← inner_smul_left],
+  congr,
+  rwa pi.smul_apply at hx,
+end
+
+instance : inner_product_space 𝕜 (Lp E 2 μ) :=
+{ norm_sq_eq_inner := norm_sq_eq_inner',
+  conj_sym := λ _ _, by simp_rw [inner_def, ← integral_conj, inner_conj_sym],
+  add_left := add_left',
+  smul_left := smul_left', }
+
+end inner_product_space
+
+end L2
+end measure_theory

src/measure_theory/lp_space.lean

@@ -1116,6 +1116,28 @@ variables [second_countable_topology E] [borel_space E]
 
 namespace lipschitz_with
 
+lemma mem_ℒp_comp_iff_of_antilipschitz {α E F} {K K'} [measurable_space α] {μ : measure α}
+  [measurable_space E] [measurable_space F] [normed_group E] [normed_group F] [borel_space E]
+  [borel_space F] [complete_space E]
+  {f : α → E} {g : E → F} (hg : lipschitz_with K g) (hg' : antilipschitz_with K' g) (g0 : g 0 = 0) :
+  mem_ℒp (g ∘ f) p μ ↔ mem_ℒp f p μ :=
+begin
+  have := ae_measurable_comp_iff_of_closed_embedding g (hg'.closed_embedding hg.uniform_continuous),
+  split,
+  { assume H,
+    have A : ∀ᵐ x ∂μ, ∥f x∥ ≤ K' * ∥g (f x)∥,
+    { apply filter.eventually_of_forall (λ x, _),
+      rw [← dist_zero_right, ← dist_zero_right, ← g0],
+      apply hg'.le_mul_dist },
+    exact H.of_le_mul (this.1 H.ae_measurable) A },
+  { assume H,
+    have A : ∀ᵐ x ∂μ, ∥g (f x)∥ ≤ K * ∥f x∥,
+    { apply filter.eventually_of_forall (λ x, _),
+      rw [← dist_zero_right, ← dist_zero_right, ← g0],
+      apply hg.dist_le_mul },
+    exact H.of_le_mul (this.2 H.ae_measurable) A }
+end
+
 /-- When `g` is a Lipschitz function sending `0` to `0` and `f` is in `Lp`, then `g ∘ f` is well
 defined as an element of `Lp`. -/
 def comp_Lp (hg : lipschitz_with c g) (g0 : g 0 = 0) (f : Lp E p μ) : Lp F p μ :=

src/measure_theory/set_integral.lean

@@ -756,14 +756,45 @@ begin
   all_goals { assumption }
 end
 
+lemma integral_comp_comm' (L : E →L[ℝ] F) {K} (hL : antilipschitz_with K L) (φ : α → E) :
+  ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
+begin
+  by_cases h : integrable φ μ,
+  { exact integral_comp_comm L h },
+  have : ¬ (integrable (L ∘ φ) μ),
+    by rwa lipschitz_with.integrable_comp_iff_of_antilipschitz L.lipschitz hL (L.map_zero),
+  simp [integral_undef, h, this]
+end
+
 lemma integral_comp_L1_comm (L : E →L[ℝ] F) (φ : α →₁[μ] E) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
 L.integral_comp_comm (L1.integrable_coe_fn φ)
 
 end continuous_linear_map
 
+namespace linear_isometry
+
+variables [measurable_space F] [borel_space F] [complete_space E]
+[second_countable_topology F] [complete_space F]
+[borel_space E] [second_countable_topology E]
+
+lemma integral_comp_comm (L : E →ₗᵢ[ℝ] F) (φ : α → E) :
+  ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ) :=
+L.to_continuous_linear_map.integral_comp_comm' L.antilipschitz _
+
+end linear_isometry
+
 variables [borel_space E] [second_countable_topology E] [complete_space E]
   [measurable_space F] [borel_space F] [second_countable_topology F] [complete_space F]
 
+@[norm_cast] lemma integral_of_real {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
+  {f : α → ℝ} :
+  ∫ a, (f a : 𝕜) ∂μ = ↑∫ a, f a ∂μ :=
+linear_isometry.integral_comp_comm is_R_or_C.of_real_li f
+
+lemma integral_conj {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {f : α → 𝕜} :
+  ∫ a, is_R_or_C.conj (f a) ∂μ = is_R_or_C.conj ∫ a, f a ∂μ :=
+linear_isometry.integral_comp_comm is_R_or_C.conj_li f
+
 lemma fst_integral {f : α → E × F} (hf : integrable f μ) :
   (∫ x, f x ∂μ).1 = ∫ x, (f x).1 ∂μ :=
 ((continuous_linear_map.fst ℝ E F).integral_comp_comm hf).symm

src/topology/metric_space/antilipschitz.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import topology.metric_space.lipschitz
+import topology.uniform_space.complete_separated
 
 /-!
 # Antilipschitz functions
@@ -121,6 +122,16 @@ begin
       rwa mul_comm } }
 end
 
+lemma closed_embedding [complete_space α]
+  (hf : antilipschitz_with K f) (hfc : uniform_continuous f) : closed_embedding f :=
+{ closed_range :=
+  begin
+    apply is_complete.is_closed,
+    rw ← complete_space_iff_is_complete_range (hf.uniform_embedding hfc),
+    apply_instance,
+  end,
+  .. (hf.uniform_embedding hfc).embedding }
+
 lemma subtype_coe (s : set α) : antilipschitz_with 1 (coe : s → α) :=
 antilipschitz_with.id.restrict s
 

src/topology/metric_space/isometry.lean

@@ -73,10 +73,14 @@ assume x y, calc
   edist ((g ∘ f) x) ((g ∘ f) y) = edist (f x) (f y) : hg _ _
                             ... = edist x y : hf _ _
 
-/-- An isometry is an embedding -/
+/-- An isometry is a uniform embedding -/
 theorem isometry.uniform_embedding (hf : isometry f) : uniform_embedding f :=
 hf.antilipschitz.uniform_embedding hf.lipschitz.uniform_continuous
 
+/-- An isometry on a complete space is a closed embedding -/
+theorem isometry.closed_embedding [complete_space α] (hf : isometry f) : closed_embedding f :=
+hf.antilipschitz.closed_embedding hf.lipschitz.uniform_continuous
+
 /-- An isometry is continuous. -/
 lemma isometry.continuous (hf : isometry f) : continuous f :=
 hf.lipschitz.continuous