From a9da37b003b0d5c7a3a4c4dc09156e82aaccf00c Mon Sep 17 00:00:00 2001 From: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Date: Tue, 24 Oct 2023 09:40:28 +0000 Subject: [PATCH] feat: volume of a complex ball (#6907) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We prove the formula for the area of a disc ```lean theorem volume_ball (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : volume (Metric.ball x r) = NNReal.pi * (ENNReal.ofReal r) ^ 2 ``` and deduce from this, the volume of complex balls ```lean theorem volume_ball (a : ℂ) (r : ℝ) : volume (Metric.ball a r) = NNReal.pi * (ENNReal.ofReal r) ^ 2 ``` Co-authored-by: James Arthur Co-authored-by: Benjamin Davidson Co-authored-by: Andrew Souther Co-authored-by: Eric Wieser --- Mathlib/Analysis/InnerProductSpace/PiL2.lean | 18 +++++++ Mathlib/Analysis/NormedSpace/WithLp.lean | 2 + .../Dynamics/Ergodic/MeasurePreserving.lean | 8 ++++ .../MeasureTheory/MeasurableSpace/Basic.lean | 4 ++ .../Measure/Haar/InnerProductSpace.lean | 47 +++++++++++++++++++ .../Measure/Lebesgue/Complex.lean | 37 ++++++++++++++- 6 files changed, 115 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean index 231d4368e6437a..02265fb1c0be54 100644 --- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean +++ b/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 diff --git a/Mathlib/Analysis/NormedSpace/WithLp.lean b/Mathlib/Analysis/NormedSpace/WithLp.lean index deef1f4ed8b634..1783bf9c60eab5 100644 --- a/Mathlib/Analysis/NormedSpace/WithLp.lean +++ b/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`. -/ diff --git a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean index b0e89a13128fdd..082ea7de7c4345 100644 --- a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean +++ b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean @@ -104,6 +104,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⟩ diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean index 4609a989c17bb1..fe75de58bee4d2 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean @@ -1315,13 +1315,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 diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean index b6a03e0f9ef5c3..a4f75ce89df440 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean +++ b/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" @@ -18,6 +20,7 @@ measure `1` to the parallelepiped spanned by any orthonormal basis, and that it the canonical `volume` from the `MeasureSpace` instance. -/ +local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 open FiniteDimensional MeasureTheory MeasureTheory.Measure Set @@ -78,6 +81,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 +104,46 @@ theorem PiLp.volume_preserving_equiv_symm : MeasurePreserving (WithLp.equiv 2 ( (EuclideanSpace.volume_preserving_measurableEquiv ι).symm end PiLp + +namespace EuclideanSpace + +open BigOperators ENNReal + +@[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 diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean index 918bdc90a58589..651fdd187fec44 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean +++ b/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" @@ -19,6 +20,7 @@ used ways to represent `ℝ²` in `mathlib`: `ℝ × ℝ` and `Fin 2 → ℝ`, d of `MeasureTheory.measurePreserving`). -/ +local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 open MeasureTheory @@ -31,11 +33,26 @@ def measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ) := basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv #align complex.measurable_equiv_pi Complex.measurableEquivPi +@[simp] +theorem measurableEquivPi_apply (a : ℂ) : + measurableEquivPi a = ![a.re, a.im] := 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 +66,22 @@ 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 +@[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