Invariance of measure

Author: loefflerd

ModularFormDimensions/Divisor.lean

@@ -11,12 +11,61 @@ import Mathlib.Algebra.Group.Action.Sum
 import Mathlib.Analysis.Meromorphic.Order
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Meromorphic.NormalForm
+import Mathlib.LinearAlgebra.Complex.Determinant
+import Mathlib.RingTheory.Norm.Transitivity
+import Mathlib.RingTheory.Complex
 
 open UpperHalfPlane Filter Topology
 
 open scoped ModularForm Manifold
 
-private lemma UpperHalfPlane.analyticAt_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
+lemma Algebra.norm_complex (a : ℂ) : Algebra.norm ℝ a = ‖a‖ ^ 2 := by
+  simp [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex,
+    Matrix.det_fin_two, RCLike.norm_sq_eq_def]
+
+/-- The derivative of the `GL(2, ℝ)`-action on `ℍ`, as an `ℝ`-linear map from `ℂ` to itself. -/
+noncomputable def UpperHalfPlane.smulFDeriv (g : GL (Fin 2) ℝ) (z : ℂ) : ℂ →L[ℝ] ℂ :=
+  (if 0 < g.det.val then ContinuousLinearEquiv.refl ℝ ℂ else Complex.conjCLE) ∘L
+  (ContinuousLinearMap.toSpanSingleton ℂ (g.det.val / denom g z ^ 2)).restrictScalars ℝ
+
+lemma det_smulFDeriv (g : GL (Fin 2) ℝ) (z : ℂ) :
+    (UpperHalfPlane.smulFDeriv g z).det =
+      SignType.sign g.det.val * g.det ^ 2 / ‖denom g z‖ ^ 4 := by
+  simp only [ContinuousLinearMap.det, smulFDeriv, ContinuousLinearEquiv.coe_refl,
+    ContinuousLinearMap.coe_comp, apply_ite, ContinuousLinearMap.coe_id,
+    ContinuousLinearMap.coe_restrictScalars, ContinuousLinearMap.toLinearMap_toSpanSingleton,
+    LinearMap.det_comp, LinearMap.det_id]
+  rw [show Complex.conjCLE.toContinuousLinearMap.toLinearMap = Complex.conjAe.toLinearMap by rfl]
+  simp only [Complex.det_conjAe]
+  rw [mul_div_assoc]
+  congr 1
+  · rcases lt_or_gt_of_ne (NeZero.ne g.det.val) with h | h
+    · simp only [not_lt.mpr h.le, ↓reduceIte, sign_neg h, SignType.coe_neg_one]
+    · simp only [h, ↓reduceIte, sign_pos h, SignType.coe_one]
+  · simp only [LinearMap.det_restrictScalars, LinearMap.det_ring, LinearMap.toSpanSingleton_apply,
+      smul_eq_mul, one_mul, Algebra.norm_complex_apply, Complex.normSq_eq_norm_sq]
+    rw [norm_div, div_pow, Complex.norm_real, ← norm_pow, Real.norm_of_nonneg (sq_nonneg _),
+      norm_pow, ← pow_mul]
+
+lemma UpperHalfPlane.hasFDerivAt_smul (g : GL (Fin 2) ℝ) (τ : ℍ) :
+    HasFDerivAt (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) (smulFDeriv g τ) τ := by
+  suffices HasFDerivAt (σ g ∘ (num g / denom g)) _ τ by
+    refine this.congr_of_eventuallyEq ?_
+    filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds τ.property] with z hz
+    simp_all [σ, coe_smul, ofComplex_apply_of_im_pos]
+  unfold UpperHalfPlane.smulFDeriv
+  apply HasFDerivAt.comp
+  · convert ContinuousLinearMap.hasFDerivAt ..
+    split_ifs with h <;>
+    · ext
+      simp [σ, h, -Matrix.GeneralLinearGroup.val_det_apply]
+  · refine (HasDerivAt.hasFDerivAt ?_).restrictScalars ℝ
+    convert HasDerivAt.div (c' := (g 0 0 : ℂ)) (d' := g 1 0) ?_ ?_ (denom_ne_zero g τ)
+    · simp [num, denom, Matrix.det_fin_two]
+      ring
+    all_goals exact (hasDerivAt_const_mul _).add_const _
+
+lemma UpperHalfPlane.analyticAt_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
     AnalyticAt ℂ (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) τ := by
   refine DifferentiableOn.analyticAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.property)
   -- surely the following must be proved in mathlib somewhere?
@@ -26,7 +75,7 @@ private lemma UpperHalfPlane.analyticAt_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.va
   unfold num denom
   exact .div (by fun_prop) (by fun_prop) fun _ hz ↦ denom_ne_zero_of_im g hz.ne'
 
-private lemma UpperHalfPlane.deriv_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
+lemma UpperHalfPlane.deriv_smul {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) (τ : ℍ) :
     deriv (fun z ↦ ↑(g • ofComplex z) : ℂ → ℂ) τ = g.val.det / denom g τ ^ 2 := by
   have : (fun z ↦ ↑(g • ofComplex z)) =ᶠ[𝓝 ↑τ] (num g / denom g) := by
     filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds τ.im_pos] with z hz
@@ -60,8 +109,7 @@ private lemma order_comp_smul {f : ℍ → ℂ} {τ : ℍ} {g : GL (Fin 2) ℝ}
   · exact τ.deriv_smul_ne_zero hg
 
 open scoped ModularForm in
-private lemma order_slash {k : ℤ} {f : ℍ → ℂ} {τ : ℍ} {g : GL (Fin 2) ℝ}
-    (hg : 0 < g.val.det) :
+private lemma order_slash {k : ℤ} {f : ℍ → ℂ} {τ : ℍ} {g : GL (Fin 2) ℝ} (hg : 0 < g.val.det) :
     meromorphicOrderAt (fun z : ℂ ↦ (f ∣[k] g) (ofComplex z)) ↑τ =
       meromorphicOrderAt (fun z ↦ f (ofComplex z)) ↑(g • τ) := by
   simp only [ModularForm.slash_def, σ, Matrix.GeneralLinearGroup.val_det_apply, hg, ↓reduceIte,

ModularFormDimensions/Measure.lean

@@ -6,6 +6,8 @@ import Mathlib.MeasureTheory.Measure.WithDensity
 import Mathlib.MeasureTheory.Function.Jacobian
 import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 
+import ModularFormDimensions.Divisor
+
 open MeasureTheory
 
 noncomputable section
@@ -21,11 +23,11 @@ lemma measurableEmbedding_coe : MeasurableEmbedding UpperHalfPlane.coe :=
 
 /-- The invariant measure on the upper half-plane, defined by `dx dy / y ^ 2`. -/
 instance : MeasureSpace ℍ :=
-  ⟨(volume.comap UpperHalfPlane.coe).withDensity fun z ↦ (1 / ⟨z.im, z.im_pos.le⟩ : NNReal) ^ 2⟩
+  ⟨(volume.comap UpperHalfPlane.coe).withDensity fun z ↦ ↑((1 / ⟨z.im, z.im_pos.le⟩ : NNReal) ^ 2)⟩
 
 /-- Express the volume of a measurable set as a lintegral over the corresponding subset of `ℂ`. -/
 lemma volume_eq_lintegral {s : Set ℍ} (hs : MeasurableSet s) :
-    volume s = ∫⁻ z : ℂ in (↑) '' s, (1 / ‖z.im‖₊) ^ 2 := by
+    volume s = ∫⁻ z : ℂ in (↑) '' s, ↑((1 / ‖z.im‖₊) ^ 2 : NNReal) := by
   simp only [volume, one_div]
   -- This proof is annoying because `setLIntegral_subtype` only works on a literal subtype,
   -- while `UpperHalfPlane` is a _type alias_ for a subtype, so we need to do some annoying
@@ -34,38 +36,55 @@ lemma volume_eq_lintegral {s : Set ℍ} (hs : MeasurableSet s) :
     ← setLIntegral_subtype (by exact isOpen_upperHalfPlaneSet.measurableSet),
     withDensity_apply _ hs]
   congr 1 with z
-  rw [ENNReal.coe_inv (mod_cast NNReal.coe_ne_zero.mp z.im_pos.ne')]
-  congr
+  congr 4
   rw [Real.norm_of_nonneg (by simpa using z.im_pos.le), ← z.coe_im,
     show UpperHalfPlane.coe = Subtype.val from rfl]
 
+/-- The measure on the upper half-plane is invariant under `GL(2, ℝ)`. -/
 instance : SMulInvariantMeasure (GL (Fin 2) ℝ) ℍ volume := by
+  -- It suffices to show `volume (g • s) = volume s` for measurable sets `s`. First
+  -- we write this as a lintegral over subsets of `ℂ`.
   refine ((smulInvariantMeasure_tfae _ _).out 2 0).mp fun g s hs ↦ ?_
   rw [volume_eq_lintegral hs, volume_eq_lintegral (hs.const_smul _)]
-
-  have aux1a (x : ℂ) (hx : x ∈ UpperHalfPlane.coe '' s) :
-        HasFDerivWithinAt (𝕜 := ℂ) (smulAux' g) (17) (UpperHalfPlane.coe '' s) x := by
-      sorry
-
-  have aux1b (x : ℂ) (hx : x ∈ UpperHalfPlane.coe '' s) :
-      HasFDerivWithinAt (𝕜 := ℝ) (smulAux' g) (
-        ContinuousLinearMap.restrictScalars ℝ (17 : ℂ →L[ℂ] ℂ)) (UpperHalfPlane.coe '' s) x :=
-    (aux1a x hx).restrictScalars ℝ
-
+  -- We want to apply the Jacobian change-of-variable formula, so first
+  -- we establish the hypotheses.
+  have aux1 (x : ℂ) (hx : x ∈ UpperHalfPlane.coe '' s) :
+      HasFDerivWithinAt (𝕜 := ℝ) (smulAux' g) (smulFDeriv g x) (UpperHalfPlane.coe '' s) x := by
+    apply HasFDerivAt.hasFDerivWithinAt
+    rcases hx with ⟨τ, hτ, rfl⟩
+    apply (UpperHalfPlane.hasFDerivAt_smul g τ).congr_of_eventuallyEq
+    filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds τ.property] with z hz
+    simp_all [σ, coe_smul, ofComplex_apply_of_im_pos, smulAux']
   have aux2 : ((↑) '' s).InjOn (smulAux' g) := by
       rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
       rw [← UpperHalfPlane.ext_iff]
       change (↑(g • x) : ℂ) = ↑(g • y) → x = y
       simp only [ext_iff', smul_left_cancel_iff, imp_self]
-
-  convert MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul
-      volume (measurableEmbedding_coe.measurableSet_image.mpr hs)
-      (fun a ha ↦ (aux1a a ha).restrictScalars ℝ) aux2
-      (fun z ↦ (1 / ‖z.im‖₊) ^ 2)
-  · have : smulAux' g ∘ ((↑) : ℍ → ℂ) = (↑) ∘ (fun x ↦ g • x) := by rfl
-    rw [← Set.image_comp, this, Set.image_comp, Set.image_smul]
-  · sorry
-
+  -- Now invoke the change-of-variable formula.
+  have main := MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul
+      volume (measurableEmbedding_coe.measurableSet_image.mpr hs) aux1 aux2
+      (fun z ↦ ↑((1 / ‖z.im‖₊) ^ 2 : NNReal))
+  -- Adjust the LHS of the resulting statement slightly to match our goal.
+  have aux3 : smulAux' g ∘ ((↑) : ℍ → ℂ) = (↑) ∘ (fun x ↦ g • x) := by rfl
+  rw [← Set.image_comp, aux3, Set.image_comp, Set.image_smul] at main
+  rw [main]
+  -- Now it remains to compare two integrals over `coe '' s`.
+  apply setLIntegral_congr_fun (measurableEmbedding_coe.measurableSet_image.mpr hs)
+  rintro _ ⟨τ, hτ, rfl⟩
+  simp only [det_smulFDeriv, abs_div, abs_mul, abs_pow, abs_pow, sq_abs,
+    (show Even 4 by grind).pow_abs]
+  have : |(SignType.sign g.det.val : ℝ)| = 1 := by
+    rcases lt_or_gt_of_ne (NeZero.ne g.det.val) with h | h <;>
+    simp [-Matrix.GeneralLinearGroup.val_det_apply, h]
+  rw [this, one_mul, ENNReal.ofReal_eq_coe_nnreal (by positivity), ← ENNReal.coe_mul,
+    ENNReal.coe_inj, NNReal.eq_iff]
+  push_cast
+  rw [div_pow, one_pow, mul_one_div, show 4 = 2 * 2 by rfl, pow_mul, ← div_pow, ← div_pow]
+  simp only [sq_eq_sq_iff_abs_eq_abs, abs_div, abs_pow, abs_one, abs_norm,
+    show smulAux' g τ = ↑(g • τ) by rfl, coe_im, im_smul_eq_div_normSq, Complex.normSq_eq_norm_sq]
+  simp only [norm_div, norm_pow, norm_mul, norm_abs_eq_norm, Real.norm_eq_abs, abs_norm]
+  rw [div_div_div_cancel_right₀ (by simpa using denom_ne_zero g τ),
+    ← div_div, div_self (by aesop)]
 
 end UpperHalfPlane