[Merged by Bors] - feat: volume of a complex ball

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -140,6 +140,24 @@ theorem EuclideanSpace.edist_eq {𝕜 : Type*} [IsROrC 𝕜] {n : Type*} [Fintyp
   PiLp.edist_eq_of_L2 x y
 #align euclidean_space.edist_eq EuclideanSpace.edist_eq
 
+theorem EuclideanSpace.ball_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
+    Metric.ball (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 < r ^ 2} := by
+  ext x
+  have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
+  simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]
+
+theorem EuclideanSpace.closedBall_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
+    Metric.closedBall (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 ≤ r ^ 2} := by
+  ext
+  simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]
+
+theorem EuclideanSpace.sphere_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
+    Metric.sphere (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 = r ^ 2} := by
+  ext x
+  have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
+  simp_rw [mem_setOf, mem_sphere_zero_iff_norm, norm_eq, norm_eq_abs, sq_abs,
+    sqrt_eq_iff_sq_eq this hr, eq_comm]
+
 variable [Fintype ι]
 
 section

Mathlib/Analysis/NormedSpace/WithLp.lean

@@ -55,6 +55,8 @@ namespace WithLp
 back and forth between the representations. -/
 protected def equiv : WithLp p V ≃ V := Equiv.refl _
 
+instance instNontrivial [Nontrivial V] : Nontrivial (WithLp p V) := ‹Nontrivial V›
+
 variable [Semiring K] [Semiring K'] [AddCommGroup V]
 
 /-! `WithLp p V` inherits various module-adjacent structures from `V`. -/

Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

@@ -99,6 +99,14 @@ protected theorem comp {g : β → γ} {f : α → β} (hg : MeasurePreserving g
   ⟨hg.1.comp hf.1, by rw [← map_map hg.1 hf.1, hf.2, hg.2]⟩
 #align measure_theory.measure_preserving.comp MeasureTheory.MeasurePreserving.comp
 
+/-- An alias of `MeasureTheory.MeasurePreserving.comp` with a convenient defeq and argument order
+for `MeasurableEquiv` -/
+protected theorem trans {e : α ≃ᵐ β} {e' : β ≃ᵐ γ}
+    {μa : Measure α} {μb : Measure β} {μc : Measure γ}
+    (h : MeasurePreserving e μa μb) (h' : MeasurePreserving e' μb μc) :
+    MeasurePreserving (e.trans e') μa μc :=
+  h'.comp h
+
 protected theorem comp_left_iff {g : α → β} {e : β ≃ᵐ γ} (h : MeasurePreserving e μb μc) :
     MeasurePreserving (e ∘ g) μa μc ↔ MeasurePreserving g μa μb := by
   refine' ⟨fun hg => _, fun hg => h.comp hg⟩

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -1219,13 +1219,17 @@ def refl (α : Type*) [MeasurableSpace α] : α ≃ᵐ α where
 instance instInhabited : Inhabited (α ≃ᵐ α) := ⟨refl α⟩
 
 /-- The composition of equivalences between measurable spaces. -/
+@[pp_dot]
 def trans (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) : α ≃ᵐ γ where
   toEquiv := ab.toEquiv.trans bc.toEquiv
   measurable_toFun := bc.measurable_toFun.comp ab.measurable_toFun
   measurable_invFun := ab.measurable_invFun.comp bc.measurable_invFun
 #align measurable_equiv.trans MeasurableEquiv.trans
 
+theorem coe_trans (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ) : ⇑(ab.trans bc) = bc ∘ ab := rfl
+
 /-- The inverse of an equivalence between measurable spaces. -/
+@[pp_dot]
 def symm (ab : α ≃ᵐ β) : β ≃ᵐ α where
   toEquiv := ab.toEquiv.symm
   measurable_toFun := ab.measurable_invFun

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.InnerProductSpace.Orientation
+import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
+import Mathlib.MeasureTheory.Measure.Lebesgue.Integral
 
 #align_import measure_theory.measure.haar.inner_product_space from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
@@ -78,6 +80,7 @@ theorem OrthonormalBasis.addHaar_eq_volume {ι F : Type*} [Fintype ι] [NormedAd
   exact b.volume_parallelepiped
 
 section PiLp
+
 variable (ι : Type*) [Fintype ι]
 
 /-- The measure equivalence between `EuclideanSpace ℝ ι` and `ι → ℝ` is volume preserving. -/
@@ -100,3 +103,49 @@ theorem PiLp.volume_preserving_equiv_symm : MeasurePreserving (WithLp.equiv 2 (
   (EuclideanSpace.volume_preserving_measurableEquiv ι).symm
 
 end PiLp
+
+namespace EuclideanSpace
+
+open BigOperators ENNReal
+
+-- See: https://github.com/leanprover/lean4/issues/2220
+local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)
+
+@[simp]
+theorem volume_ball (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) :
+    volume (Metric.ball x r) = NNReal.pi * (ENNReal.ofReal r) ^ 2 := by
+  obtain hr | hr := le_total r 0
+  · rw [Metric.ball_eq_empty.mpr hr, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow zero_lt_two,
+      mul_zero]
+  · suffices volume (Metric.ball (0 : EuclideanSpace ℝ (Fin 2)) 1) = NNReal.pi by
+      rw [Measure.addHaar_ball _ _ hr, finrank_euclideanSpace_fin, ofReal_pow hr, this, mul_comm]
+    calc
+      _ = volume {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 < 1} := by
+        have : MeasurePreserving (_ : ℝ × ℝ ≃ᵐ EuclideanSpace ℝ (Fin 2)) :=
+          MeasurePreserving.trans
+            (volume_preserving_finTwoArrow ℝ).symm (volume_preserving_measurableEquiv (Fin 2)).symm
+        rw [←this.measure_preimage_emb (MeasurableEquiv.measurableEmbedding _),
+          ball_zero_eq _ zero_le_one, preimage_setOf_eq]
+        simp only [MeasurableEquiv.finTwoArrow_symm_apply, Fin.sum_univ_two, preimage_setOf_eq,
+          Fin.cons_zero, Fin.cons_one, one_pow, Function.comp_apply, coe_measurableEquiv_symm,
+          MeasurableEquiv.trans_apply, WithLp.equiv_symm_pi_apply]
+      _ = volume {p : ℝ × ℝ | (- 1 < p.1 ∧ p.1 ≤ 1) ∧ p.1 ^ 2 + p.2 ^ 2 < 1} := by
+        congr
+        refine Set.ext fun _ => iff_and_self.mpr fun h => And.imp_right le_of_lt ?_
+        rw [← abs_lt, ← sq_lt_one_iff_abs_lt_one]
+        exact lt_of_add_lt_of_nonneg_left h (sq_nonneg _)
+      _ = volume (regionBetween (fun x => - Real.sqrt (1 - x ^ 2)) (fun x => Real.sqrt (1 - x ^ 2))
+          (Set.Ioc (-1) 1)) := by
+        simp_rw [regionBetween, Set.mem_Ioo, Set.mem_Ioc, ← Real.sq_lt, lt_tsub_iff_left,
+          Nat.cast_one]
+      _ = ENNReal.ofReal ((2 : ℝ) * ∫ (a : ℝ) in Set.Ioc (-1) 1, Real.sqrt (1 - a ^ 2)) := by
+        rw [volume_eq_prod, volume_regionBetween_eq_integral (Continuous.integrableOn_Ioc
+          (by continuity)) (Continuous.integrableOn_Ioc (by continuity)) measurableSet_Ioc
+          (fun _ _ => neg_le_self (Real.sqrt_nonneg _))]
+        simp_rw [Pi.sub_apply, sub_neg_eq_add, ← two_mul, integral_mul_left]
+      _ = NNReal.pi := by
+        rw [← intervalIntegral.integral_of_le (by norm_num : (-1 : ℝ) ≤ 1), Nat.cast_one,
+          integral_sqrt_one_sub_sq, two_mul, add_halves, ← NNReal.coe_real_pi,
+          ofReal_coe_nnreal]
+
+end EuclideanSpace

Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean

@@ -3,8 +3,9 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
+import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
+import Mathlib.MeasureTheory.Measure.Lebesgue.Integral
 
 #align_import measure_theory.measure.lebesgue.complex from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
 
@@ -31,11 +32,26 @@ def measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ) :=
   basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv
 #align complex.measurable_equiv_pi Complex.measurableEquivPi
 
+@[simp]
+theorem measurableEquivPi_apply (a : ℂ) :
+    measurableEquivPi a = Fin.cons a.re (Fin.cons a.im finZeroElim) := rfl
+
+@[simp]
+theorem measurableEquivPi_symm_apply (p : (Fin 2) → ℝ) :
+    measurableEquivPi.symm p = (p 0) + (p 1) * I := rfl
+
 /-- Measurable equivalence between `ℂ` and `ℝ × ℝ`. -/
 def measurableEquivRealProd : ℂ ≃ᵐ ℝ × ℝ :=
   equivRealProdClm.toHomeomorph.toMeasurableEquiv
 #align complex.measurable_equiv_real_prod Complex.measurableEquivRealProd
 
+@[simp]
+theorem measurableEquivRealProd_apply (a : ℂ) : measurableEquivRealProd a = (a.re, a.im) := rfl
+
+@[simp]
+theorem measurableEquivRealProd_symm_apply (p : ℝ × ℝ) :
+    measurableEquivRealProd.symm p = {re := p.1, im := p.2} := rfl
+
 theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi := by
   convert (measurableEquivPi.symm.measurable.measurePreserving volume).symm
   rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
@@ -49,4 +65,25 @@ theorem volume_preserving_equiv_real_prod : MeasurePreserving measurableEquivRea
   (volume_preserving_finTwoArrow ℝ).comp volume_preserving_equiv_pi
 #align complex.volume_preserving_equiv_real_prod Complex.volume_preserving_equiv_real_prod
 
+-- See: https://github.com/leanprover/lean4/issues/2220
+local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)
+
+@[simp]
+theorem volume_ball (a : ℂ) (r : ℝ) :
+    volume (Metric.ball a r) = NNReal.pi * (ENNReal.ofReal r) ^ 2 := by
+  rw [Measure.addHaar_ball_center, ← EuclideanSpace.volume_ball 0,
+    ← (volume_preserving_equiv_pi.symm).measure_preimage measurableSet_ball,
+    ← ((EuclideanSpace.volume_preserving_measurableEquiv (Fin 2)).symm).measure_preimage
+    measurableSet_ball]
+  refine congrArg _ (Set.ext fun _ => ?_)
+  simp_rw [← MeasurableEquiv.coe_toEquiv_symm, Set.mem_preimage, MeasurableEquiv.coe_toEquiv_symm,
+    measurableEquivPi_symm_apply, mem_ball_zero_iff, norm_eq_abs, abs_def, normSq_add_mul_I,
+    EuclideanSpace.coe_measurableEquiv_symm, EuclideanSpace.norm_eq, WithLp.equiv_symm_pi_apply,
+    Fin.sum_univ_two, Real.norm_eq_abs, _root_.sq_abs]
+
+@[simp]
+theorem volume_closedBall (a : ℂ) (r : ℝ) :
+     volume (Metric.closedBall a r) = NNReal.pi * (ENNReal.ofReal r) ^ 2 := by
+  rw [MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball, Complex.volume_ball]
+
 end Complex