import Definitions.Def_HaarQuotient import Definitions.Def_LanglandsTunnell_CubicInduction_Structure import Definitions.Def_NumberField_TateGlobalZeta import Definitions.Def_M4aHerbrand_AdeleTopologyFacts set_option autoImplicit false noncomputable section open MeasureTheory IsDedekindDomain NumberField NumberField.AdelicHaar LanglandsTunnell.CubicInduction Topology open scoped ENNReal NNReal namespace WhittakerBlock def unipotentSubgroup3 : Subgroup (AdelicGL 3 (π“ž β„š) β„š) := Subgroup.closure (Set.range fun t : AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š => upperUnipotent3 t.1 t.2.1 t.2.2) def unipotentHaar3 : @Measure β†₯unipotentSubgroup3 (@Subtype.instMeasurableSpace _ _ (glBorel (Fin 3) (π“ž β„š) β„š)) := letI : MeasurableSpace (AdeleRing (π“ž β„š) β„š) := adeleBorel (π“ž β„š) β„š letI : MeasurableSpace (AdelicGL 3 (π“ž β„š) β„š) := glBorel (Fin 3) (π“ž β„š) β„š Measure.map (fun t : AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š Γ— AdeleRing (π“ž β„š) β„š => (⟨upperUnipotent3 t.1 t.2.1 t.2.2, Subgroup.subset_closure ⟨t, rfl⟩⟩ : unipotentSubgroup3)) ((adelicAddHaar (π“ž β„š) β„š).prod ((adelicAddHaar (π“ž β„š) β„š).prod (adelicAddHaar (π“ž β„š) β„š))) def quotientMeasure : @Measure (MulAction.orbitRel.Quotient (unipotentSubgroup3) (AdelicGL 3 (π“ž β„š) β„š)) (@Quotient.instMeasurableSpace _ _ (glBorel (Fin 3) (π“ž β„š) β„š)) := letI : MeasurableSpace (AdelicGL 3 (π“ž β„š) β„š) := glBorel (Fin 3) (π“ž β„š) β„š HaarQuotient.measure (adelicGLHaar (Fin 3) (π“ž β„š) β„š) unipotentSubgroup3 unipotentHaar3 def zerothShell (S : Finset (HeightOneSpectrum (π“ž β„š))) : Set (MulAction.orbitRel.Quotient (unipotentSubgroup3) (AdelicGL 3 (π“ž β„š) β„š)) := {q | βˆ€ p : HeightOneSpectrum (π“ž β„š), p βˆ‰ S β†’ βˆƒ (x y z : p.adicCompletion β„š) (k : GL (Fin 3) (p.adicCompletion β„š)), k ∈ localMaximalCompact3 (π“ž β„š) β„š p ∧ componentAt3 (π“ž β„š) β„š p q.out = upperUnipotent3 x y z * k} def block (pins : AutomorphicForm.CarrierPins β„š) (ψ : AddChar (AdeleRing (π“ž β„š) β„š) β„‚) (f : AdelicGL 3 (π“ž β„š) β„š β†’ β„‚) (Ξ¦ : (Fin 3 β†’ AdeleRing (π“ž β„š) β„š) β†’ β„‚) (Οƒ : ℝ) (S : Finset (HeightOneSpectrum (π“ž β„š))) : ℝβ‰₯0∞ := letI : MeasurableSpace (AdelicGL 3 (π“ž β„š) β„š) := glBorel (Fin 3) (π“ž β„š) β„š ∫⁻ q in zerothShell S, ((β€–whittaker3 pins ψ f q.outβ€–β‚Š : ℝβ‰₯0∞) ^ 2 * (β€–Ξ¦ fun j : Fin 3 => (q.out : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 jβ€–β‚Š : ℝβ‰₯0∞) * ENNReal.ofReal (NumberField.TateGlobal.ideleNorm β„š (Matrix.GeneralLinearGroup.det q.out) ^ Οƒ)) βˆ‚quotientMeasure instance sigmaCompactSpace_adelicGL3 : SigmaCompactSpace (AdelicGL 3 (π“ž β„š) β„š) := by haveI : SigmaCompactSpace (Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) := inferInstanceAs (SigmaCompactSpace (Fin 3 β†’ Fin 3 β†’ AdeleRing (π“ž β„š) β„š)) haveI : SigmaCompactSpace (Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š))ᡐᡒᡖ := MulOpposite.opHomeomorph.symm.isClosedEmbedding.sigmaCompactSpace exact Units.isClosedEmbedding_embedProduct.sigmaCompactSpace section Heisenberg variable {A : Type*} [CommRing A] private theorem upperUnipotent3_mul (x y z x' y' z' : A) : upperUnipotent3 x y z * upperUnipotent3 x' y' z' = upperUnipotent3 (x + x') (y + y') (z + z' + x * y') := by ext i j fin_cases i <;> fin_cases j <;> simp [upperUnipotent3, Units.val_mul, Matrix.mul_apply, Fin.sum_univ_three] all_goals ring private theorem upperUnipotent3_inv (x y z : A) : (upperUnipotent3 x y z)⁻¹ = upperUnipotent3 (-x) (-y) (x * y - z) := by rw [inv_eq_iff_mul_eq_one, upperUnipotent3_mul, show x + -x = 0 by ring, show y + -y = 0 by ring, show z + (x * y - z) + x * -y = 0 by ring, upperUnipotent3_zero] end Heisenberg theorem mem_unipotentSubgroup3_iff (g : AdelicGL 3 (π“ž β„š) β„š) : g ∈ unipotentSubgroup3 ↔ βˆƒ x y z : AdeleRing (π“ž β„š) β„š, g = upperUnipotent3 x y z := by refine ⟨fun hg => ?_, fun ⟨x, y, z, h⟩ => h β–Έ Subgroup.subset_closure ⟨(x, y, z), rfl⟩⟩ unfold unipotentSubgroup3 at hg induction hg using Subgroup.closure_induction with | mem _ h => obtain ⟨t, rfl⟩ := h; exact ⟨t.1, t.2.1, t.2.2, rfl⟩ | one => exact ⟨0, 0, 0, upperUnipotent3_zero.symm⟩ | mul _ _ _ _ h h' => obtain ⟨x, y, z, rfl⟩ := h obtain ⟨x', y', z', rfl⟩ := h' exact ⟨_, _, _, upperUnipotent3_mul x y z x' y' z'⟩ | inv _ _ h => obtain ⟨x, y, z, rfl⟩ := h exact ⟨_, _, _, upperUnipotent3_inv x y z⟩ theorem coe_unipotentSubgroup3_eq : ((unipotentSubgroup3 : Subgroup (AdelicGL 3 (π“ž β„š) β„š)) : Set (AdelicGL 3 (π“ž β„š) β„š)) = {g : AdelicGL 3 (π“ž β„š) β„š | (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 0 0 = 1 ∧ (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 1 1 = 1 ∧ (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 2 = 1 ∧ (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 1 0 = 0 ∧ (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 0 = 0 ∧ (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 2 1 = 0} := by ext g simp only [SetLike.mem_coe, Set.mem_setOf_eq, mem_unipotentSubgroup3_iff] constructor Β· rintro ⟨x, y, z, rfl⟩ simp Β· rintro ⟨h00, h11, h22, h10, h20, h21⟩ refine ⟨(g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 0 1, (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 1 2, (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) 0 2, ?_⟩ refine Matrix.GeneralLinearGroup.ext fun i j => ?_ rw [upperUnipotent3_coe] fin_cases i <;> fin_cases j <;> simp [h00, h11, h22, h10, h20, h21] theorem isClosed_unipotentSubgroup3 : IsClosed ((unipotentSubgroup3 : Subgroup (AdelicGL 3 (π“ž β„š) β„š)) : Set (AdelicGL 3 (π“ž β„š) β„š)) := by rw [coe_unipotentSubgroup3_eq] have hc : βˆ€ i j : Fin 3, Continuous fun g : AdelicGL 3 (π“ž β„š) β„š => (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) i j := fun i j => Units.continuous_val.matrix_elem i j have hz : βˆ€ (i j : Fin 3) (c : AdeleRing (π“ž β„š) β„š), IsClosed {g : AdelicGL 3 (π“ž β„š) β„š | (g : Matrix (Fin 3) (Fin 3) (AdeleRing (π“ž β„š) β„š)) i j = c} := fun i j c => isClosed_singleton.preimage (hc i j) simp only [Set.setOf_and] exact (hz 0 0 1).inter ((hz 1 1 1).inter ((hz 2 2 1).inter ((hz 1 0 0).inter ((hz 2 0 0).inter (hz 2 1 0))))) end WhittakerBlock end