BorelJacquet.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

43 declarations, 0 contain sorry, 0 declared as axioms

Automorphic forms in the sense of Borel-Jacquet

Borel-Jacquet means the definition of an automorphic form given by Armand Borel and Hervé Jacquet in their article in the Corvallis proceedings (the first reference below) — the standard adelic definition. It is formalised here for G = GL n / ℚ with maximal compact subgroup K = O n ℝ, in the shape Buzzard states it for GL₂.

Writing G(𝔸) = G(𝔸_f) × G(ℝ), where G(𝔸_f) = GL n 𝔸ᶠ[ℤ, ℚ] is the points of GL n in the finite adeles of ℚ, an automorphic form is a smooth f : G(𝔸) → ℂ such that

(a) f (γ x) = f x for all γ ∈ G(ℚ), embedded diagonally;
(b1) f (x u) = f x for all u in some compact open subgroup of G(𝔸_f);
(b2) the ℂ-span of the right translates x ↦ f (x k), for k ∈ K, is finite-dimensional;
(c) f is annihilated by an ideal of finite codimension of the centre of the universal enveloping algebra of the complexified Lie algebra of G(ℝ), acting by left invariant differential operators;
(d) for each x ∈ G(𝔸_f), the function y ↦ f (x, y) on G(ℝ) is slowly increasing.

Smooth means continuous, locally constant in the finite variable and C^∞ in the archimedean one. The further condition (e) cutting out cusp forms, that the constant term along every unipotent radical vanishes, is not formalised here: it needs Haar integration over N(ℚ) \ N(𝔸).

Main declarations

All in the namespace Matrix.GeneralLinearGroup unless qualified otherwise:

AutomorphicForm.IsKFinite and AutomorphicForm.IsZFinite: the finiteness conditions (b2) and (c), for an abstract group and module respectively.
gnorm and IsSlowlyIncreasing: the norm ‖y‖ = max (|y|, |y⁻¹|) on GL n ℝ and condition (d), slow increase.
IsSmoothAdelic and IsAutomorphicForm: smoothness on G(𝔸), and the definition itself.
isAutomorphicForm_one: the constant function 1 is an automorphic form — a sanity check exercising every condition; condition (c) holds through constantsCharacter, the character by which the centre acts on constants.
automorphicForms and rightTranslation: the automorphic forms as a ℂ-submodule of the functions on G(𝔸), with the right translation representation of G(𝔸_f) on it.

The remaining ingredients of the definition are developed in the BorelJacquet subdirectory:

BorelJacquet.LieDeriv: the C^∞ functions on GL n ℝ (IsSmoothOnGL, smoothGL) and the action on them of 𝔤𝔩 n ℝ and its complexification (lieDeriv, lieDerivC).
BorelJacquet.CenterAction: the enveloping algebra universalEnveloping, its centre centerUniversalEnveloping, their action (envelopingAction, centerAction) — the action of condition (c) — and the character constantsCharacter.
BorelJacquet.Subgroups: the subgroups ratDiagonal (condition (a)), orthogonalSubgroup (condition (b2)) and integralAdelicSubgroup (the compact open subgroup witnessing condition (b1)).

Relation to the literature

Buzzard states (b2) through a finite-dimensional representation σ of K; for compact K that formulation is equivalent to the one used here, since the span of the translates is a continuous, hence semisimple, finite-dimensional representation of K. Conditions (b1) and (b2) together are the K-finiteness of Getz-Hahn's Definition 6.5 for K = K_∞ K^∞ with K^∞ ≤ G(𝔸_f) compact open.

Condition (d) follows Buzzard in letting the constants depend on the finite variable. Getz-Hahn's Definition 6.4 instead imposes one global bound |f g| ≤ c * H g ^ r for their adelic height H; for GL n that height factors as H (x, y) = H_f x * gnorm y, so the global bound implies (d). Only these implications are asserted; no equivalence with Getz-Hahn's full definition is claimed.

Implementation notes

The action of condition (c) is constructed, not assumed; see FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.LieDeriv and FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.CenterAction for the construction. The action lives on smoothGL n, not on all of G(𝔸) → ℂ — a differential operator has nothing to act on at a non-differentiable function — so condition (c) asks for one ideal annihilating every slice y ↦ f (x, y) at once, the finite variable being a spectator.

References:

A. Borel and H. Jacquet, Automorphic forms and automorphic representations, in Automorphic Forms, Representations and L-functions (Corvallis), Proc. Sympos. Pure Math. 33, Part 1, Amer. Math. Soc. (1979), 189–207; §4.
K. Buzzard, Automorphic forms for GL2 over Q, §1. https://www.ma.imperial.ac.uk/~buzzard/maths/research/notes/automorphic_forms_for_gl2_over_Q.pdf
J. R. Getz and H. Hahn, An Introduction to Automorphic Representations, GTM 300, Springer (2024), §6.2 and §6.3; in the numbering of that text, Definitions 6.1 (moderate growth), 6.2 (Z(𝔤)-finiteness), 6.4 (adelic moderate growth) and 6.5 (adelic automorphic form). https://sites.duke.edu/jgetz/files/2022/04/Graduate_Text.pdf

Imports (8)

Imported by 1 file

FormalConjecturesForMathlib.lean

def AutomorphicForm.rightTranslateSpan The k-span of the right translates of f by the subgroup K line 125 source
Source documentation
The k-span of the right translates of f by the subgroup K.

standard axioms: Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field, Submodule
Proof uses: Submodule.span, Set.range, Subtype, Membership.mem, HMul.hMul
23 instances, coercions and auxiliary constants left out.
```
def rightTranslateSpan : Submodule k (G → k) :=
…
```
lemma AutomorphicForm.self_mem_rightTranslateSpan line 128 source
standard axioms: Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field, Membership.mem, Submodule, AutomorphicForm.rightTranslateSpan
Proof uses: Submodule.subset_span, Set.range, Subtype, HMul.hMul, Exists.intro, Eq, OfNat.ofNat, funext, of_eq_true, Eq.trans, True, congrFun', congrArg, mul_one, eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
abbrev AutomorphicForm.IsKFinite f is K-finite: the span of its right K-translates is finite-dimensional line 133 source
Source documentation
f is K-finite: the span of its right K-translates is finite-dimensional. This is condition (b2) in the definition of an automorphic form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field
Proof uses: FiniteDimensional, Subtype, Membership.mem, Submodule, AutomorphicForm.rightTranslateSpan
15 instances, coercions and auxiliary constants left out.
```
abbrev IsKFinite : Prop := FiniteDimensional k (rightTranslateSpan K k f)
…
```
Mentions: AutomorphicForm.rightTranslateSpan
lemma AutomorphicForm.isKFinite_of_rightInvariant A function invariant under right translation by K is K-finite line 138 source
Source documentation
A function invariant under right translation by K is K-finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field, Subtype, Membership.mem, Eq, HMul.hMul, AutomorphicForm.IsKFinite
Proof uses: FiniteDimensional.span_of_finite, Set.range, Set.Finite.subset, Singleton.singleton, Set, Set.finite_singleton, Iff.mpr, LE.le, Set.range_subset_iff, funext
31 instances, coercions and auxiliary constants left out.
```
lemma isKFinite_of_rightInvariant (h : ∀ (x : G) (u : K), f (x * (u : G)) = f x) :
    IsKFinite K k f :=
…
```
Mentions: AutomorphicForm.IsKFinite
lemma AutomorphicForm.isKFinite_of_finite If K is finite then every function is K-finite line 144 source
Source documentation
If K is finite then every function is K-finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field, Finite, Subtype, Membership.mem, AutomorphicForm.IsKFinite
Proof uses: FiniteDimensional.span_of_finite, Set.range, HMul.hMul, Set.finite_range
21 instances, coercions and auxiliary constants left out.
```
lemma isKFinite_of_finite [Finite K] : IsKFinite K k f :=
…
```
Mentions: AutomorphicForm.IsKFinite
lemma AutomorphicForm.IsKFinite.add K-finiteness is closed under addition: the translate span of f + g sits inside the sum of the translate spans line 149 source
Source documentation
K-finiteness is closed under addition: the translate span of f + g sits inside the sum of the translate spans.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field, AutomorphicForm.IsKFinite, HAdd.hAdd
Proof uses: Submodule.finiteDimensional_of_le, AutomorphicForm.rightTranslateSpan, Max.max, Submodule, Iff.mpr, LE.le, Submodule.span, Set.range, Subtype, Membership.mem, HMul.hMul, Set, Submodule.span_le, Set.range_subset_iff, AddMemClass.add_mem, Submodule.mem_sup_left, Submodule.subset_span, Exists.intro, Eq, rfl and 1 more
52 instances, coercions and auxiliary constants left out.
```
protected lemma IsKFinite.add {f g : G → k} (hf : IsKFinite K k f) (hg : IsKFinite K k g) :
    IsKFinite K k (f + g) :=
…
```
Mentions: AutomorphicForm.IsKFinite
lemma AutomorphicForm.IsKFinite.const_smul line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Field, AutomorphicForm.IsKFinite, HSMul.hSMul
Proof uses: Submodule.finiteDimensional_of_le, AutomorphicForm.rightTranslateSpan, Iff.mpr, LE.le, Submodule, Submodule.span, Set.range, Subtype, Membership.mem, HMul.hMul, Set, Submodule.span_le, Set.range_subset_iff, Submodule.smul_mem, Submodule.subset_span, Exists.intro, Eq, rfl
40 instances, coercions and auxiliary constants left out.
def AutomorphicForm.IsZFinite m is Z-finite: it is annihilated by an ideal of Z of finite codimension over k line 176 source
Source documentation
m is Z-finite: it is annihilated by an ideal of Z of finite codimension over k. This is condition (c), with Z the centre of the universal enveloping algebra of the complexified Lie algebra of G(ℝ), i.e. Matrix.GeneralLinearGroup.centerUniversalEnveloping n.
This is Getz-Hahn's Definition 6.2, in the form they state for a vector of an arbitrary Z(𝔤)-module. They note it is equivalent to Z • m being finite-dimensional over k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module
Proof uses: Exists, Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, Eq, HSMul.hSMul, OfNat.ofNat
43 instances, coercions and auxiliary constants left out.
```
def IsZFinite (m : M) : Prop :=
…
```
lemma AutomorphicForm.isZFinite_zero line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, AutomorphicForm.IsZFinite, OfNat.ofNat
Proof uses: Exists.intro, Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, Eq, HSMul.hSMul, Top.top, And.intro, inferInstance, smul_zero
55 instances, coercions and auxiliary constants left out.
lemma AutomorphicForm.IsZFinite.add Z-finiteness is closed under addition: the intersection of the two annihilating ideals works, since Z ⧸ (I ⊓ J) embeds in (Z ⧸ I) × (Z ⧸ J) line 185 source
Source documentation
Z-finiteness is closed under addition: the intersection of the two annihilating ideals works, since Z ⧸ (I ⊓ J) embeds in (Z ⧸ I) × (Z ⧸ J).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, AutomorphicForm.IsZFinite, HAdd.hAdd
Proof uses: Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, Eq, HSMul.hSMul, OfNat.ofNat, Submodule, LinearMap.ker, Prod, RingHom.id, LinearMap.prod, Submodule.mkQ, Min.min, of_eq_true, Eq.trans, True, congrFun', congrArg and 21 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
protected lemma IsZFinite.add {m₁ m₂ : M} (h₁ : IsZFinite k Z m₁) (h₂ : IsZFinite k Z m₂) :
    IsZFinite k Z (m₁ + m₂) := by
…
```
Mentions: AutomorphicForm.IsZFinite
lemma AutomorphicForm.IsZFinite.const_smul Z-finiteness is preserved by scalar multiplication: the same ideal works line 194 source
Source documentation
Z-finiteness is preserved by scalar multiplication: the same ideal works.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, IsScalarTower, AutomorphicForm.IsZFinite, HSMul.hSMul
Proof uses: Exists.imp, Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, Eq, OfNat.ofNat, And.imp_right, Eq.mpr, RingHom, Algebra.algebraMap, id, congrArg, Eq.symm, algebraMap_smul, HMul.hMul, smul_smul, mul_comm, smul_zero and 1 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
protected lemma IsZFinite.const_smul [Module k M] [IsScalarTower k Z M] {m : M}
    (h : IsZFinite k Z m) (c : k) : IsZFinite k Z (c • m) :=
…
```
Mentions: AutomorphicForm.IsZFinite, c
lemma AutomorphicForm.IsZFinite.of_forall_smul_eq_algHom_smul An element on which Z acts through a k-algebra character is Z-finite: the kernel of the character is an ideal of finite codimension annihilating it line 201 source
Source documentation
An element on which Z acts through a k-algebra character is Z-finite: the kernel of the character is an ideal of finite codimension annihilating it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, AlgHom, Eq, HSMul.hSMul, AutomorphicForm.IsZFinite
Proof uses: Exists.intro, Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, OfNat.ofNat, RingHom.ker, And.intro, FiniteDimensional.of_injective, AlgHom.toLinearMap, Ideal.kerLiftAlg, Ideal.kerLiftAlg_injective, Eq.mpr, id, congrArg, Iff.mp, RingHom.mem_ker, zero_smul, Eq.refl
79 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma IsZFinite.of_forall_smul_eq_algHom_smul [Module k M] (χ : Z →ₐ[k] k) {m : M}
    (h : ∀ z, z • m = χ z • m) : IsZFinite k Z m :=
…
```
Mentions: AutomorphicForm.IsZFinite
lemma AutomorphicForm.IsZFinite.pi_const A constant family with Z-finite value is Z-finite, with the same ideal line 207 source
Source documentation
A constant family with Z-finite value is Z-finite, with the same ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, AutomorphicForm.IsZFinite
Proof uses: Exists.imp, Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, Eq, HSMul.hSMul, OfNat.ofNat, And.imp_right, funext
47 instances, coercions and auxiliary constants left out.
```
protected lemma IsZFinite.pi_const {ι : Type*} {m₀ : M} (h : IsZFinite k Z m₀) :
    IsZFinite k Z (fun _ : ι => m₀) :=
…
```
Mentions: AutomorphicForm.IsZFinite
lemma AutomorphicForm.IsZFinite.comp Precomposition preserves Z-finiteness of a family, with the same ideal line 212 source
Source documentation
Precomposition preserves Z-finiteness of a family, with the same ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, AutomorphicForm.IsZFinite, Function.comp
Proof uses: Exists.imp, Ideal, And, FiniteDimensional, HasQuotient.Quotient, Membership.mem, Eq, HSMul.hSMul, OfNat.ofNat, And.imp_right, funext, congrFun
47 instances, coercions and auxiliary constants left out.
```
protected lemma IsZFinite.comp {ι' ι : Type*} {m : ι → M} (h : IsZFinite k Z m) (σ : ι' → ι) :
    IsZFinite k Z (m ∘ σ) :=
…
```
Mentions: AutomorphicForm.IsZFinite
def Matrix.GeneralLinearGroup.entrySup The sup norm on the entries of a matrix: for n = 2 this is |(a b; c d)| = max {|a|, |b|, |c|, |d|} line 235 source
Source documentation
The sup norm on the entries of a matrix: for n = 2 this is |(a b; c d)| = max {|a|, |b|, |c|, |d|}.
The supremum is taken in ℝ≥0 rather than ℝ so that it is also defined when n is empty, where it takes the value 0 — the right answer, since then Matrix n n ℝ is the zero ring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Real
Proof uses: Finset.sup, NNReal, Finset.univ, NNNorm.nnnorm
10 instances, coercions and auxiliary constants left out.
```
noncomputable def entrySup (M : Matrix n n ℝ) : ℝ :=
…
```
lemma Matrix.GeneralLinearGroup.le_entrySup line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Real, LE.le, abs, Matrix.GeneralLinearGroup.entrySup
Proof uses: NNReal, NNNorm.nnnorm, Finset.sup, Finset.univ, LE.le.trans, Finset.le_sup, Finset.mem_univ, Eq.mpr, id, Eq, Iff.mpr, NNReal.coe_le_coe
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.entrySup_nonneg line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Matrix, Real, LE.le, OfNat.ofNat, Matrix.GeneralLinearGroup.entrySup
Proof uses: id, NNReal.coe_nonneg, Finset.sup, NNReal, Finset.univ, NNNorm.nnnorm
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.gnorm The norm ‖y‖ = max (|y|, |y⁻¹|) on GL n ℝ, with |·| the sup norm on matrix entries line 255 source
Source documentation
The norm ‖y‖ = max (|y|, |y⁻¹|) on GL n ℝ, with |·| the sup norm on matrix entries. This is the norm used to define slow increase.
For G = GL n this is exactly the archimedean factor of the norm Getz-Hahn use for a general reductive G: theirs is the sup of the entries of ι y, for ι : G → SL (2 * n) the embedding y ↦ (y, (y⁻¹)ᵗ), whose entries are those of y together with those of y⁻¹.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real
Proof uses: Max.max, Matrix.GeneralLinearGroup.entrySup, Matrix, Inv.inv
7 instances, coercions and auxiliary constants left out.
```
noncomputable def gnorm (y : GL n ℝ) : ℝ :=
…
```
lemma Matrix.GeneralLinearGroup.gnorm_nonneg line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, LE.le, OfNat.ofNat, Matrix.GeneralLinearGroup.gnorm
Proof uses: le_max_of_le_left, Matrix.GeneralLinearGroup.entrySup, Matrix, Inv.inv, Matrix.GeneralLinearGroup.entrySup_nonneg
12 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.gnorm_inv line 262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Eq, Matrix.GeneralLinearGroup.gnorm, Inv.inv, Matrix
Proof uses: Eq.mpr, Max.max, Matrix.GeneralLinearGroup.entrySup, id, congrArg, Matrix.GeneralLinearGroup.gnorm.eq_1, inv_inv, max_comm, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.inv_card_le_gnorm gnorm is uniformly bounded below: since y * y⁻¹ = 1, the entries of y and y⁻¹ cannot all be small line 268 source
Source documentation
gnorm is uniformly bounded below: since y * y⁻¹ = 1, the entries of y and y⁻¹ cannot all be small. This makes the exponent in a slow-increase bound enlargeable, hence IsSlowlyIncreasing closed under addition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, LE.le, Inv.inv, Fintype.card, Matrix.GeneralLinearGroup.gnorm
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Eq.mpr, OfNat.ofNat, id, Eq, congrFun', congrArg, Eq.trans, Nat, Fintype.card_eq_zero, CharP.cast_eq_zero, inv_zero, Matrix.GeneralLinearGroup.gnorm_nonneg, cast, Eq.symm, Nat.cast_one, Iff.mpr and 97 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma inv_card_le_gnorm (y : GL n ℝ) : (Fintype.card n : ℝ)⁻¹ ≤ gnorm y := by
…
```
Mentions: Matrix.GeneralLinearGroup.gnorm
lemma Matrix.GeneralLinearGroup.gnorm_pos line 286 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nonempty, Matrix.GeneralLinearGroup, Real, LT.lt, OfNat.ofNat, Matrix.GeneralLinearGroup.gnorm
Proof uses: LT.lt.trans_le, Inv.inv, Fintype.card, Iff.mpr, inv_pos, cast, Nat, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Fintype.card_pos, Matrix.GeneralLinearGroup.inv_card_le_gnorm
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.IsSlowlyIncreasing A function φ : GL n ℝ → ℂ is slowly increasing, or of moderate growth, if ‖φ y‖ ≤ C * ‖y‖ ^ r for some real C and natural number r line 296 source
Source documentation
A function φ : GL n ℝ → ℂ is slowly increasing, or of moderate growth, if ‖φ y‖ ≤ C * ‖y‖ ^ r for some real C and natural number r. This is condition (d) in the definition of an automorphic form.
Taking the exponent to be a natural number rather than a real is no loss — a real exponent can always be rounded up, since gnorm ≥ 1 / Fintype.card n — and it makes the definition come out right for GL 0, where gnorm is identically 0 and (0 : ℝ) ^ (0 : ℕ) = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex
Proof uses: Exists, Nat, LE.le, Norm.norm, HMul.hMul, HPow.hPow, Matrix.GeneralLinearGroup.gnorm
10 instances, coercions and auxiliary constants left out.
```
def IsSlowlyIncreasing (φ : GL n ℝ → ℂ) : Prop :=
…
```
lemma Matrix.GeneralLinearGroup.IsSlowlyIncreasing.of_bounded line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, LE.le, Norm.norm, Matrix.GeneralLinearGroup.IsSlowlyIncreasing
Proof uses: Exists.intro, Exists, Nat, HMul.hMul, HPow.hPow, Matrix.GeneralLinearGroup.gnorm, OfNat.ofNat, Eq.mpr, id, Eq, congrArg, Eq.trans, pow_zero, mul_one
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.isSlowlyIncreasing_const line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Complex, Matrix.GeneralLinearGroup.IsSlowlyIncreasing, Matrix.GeneralLinearGroup, Real
Proof uses: Matrix.GeneralLinearGroup.IsSlowlyIncreasing.of_bounded, Norm.norm, le_rfl
4 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.IsSlowlyIncreasing.const_mul line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSlowlyIncreasing, HMul.hMul
Proof uses: Exists, Nat, LE.le, Norm.norm, HPow.hPow, Matrix.GeneralLinearGroup.gnorm, Exists.intro, Eq.mpr, id, Eq, congrArg, norm_mul, mul_assoc, mul_le_mul_of_nonneg_left, norm_nonneg
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.exists_forall_norm_le_pow_of_le Documented declaration: exists_forall_norm_le_pow_of_le line 316 source
Source documentation
A slow-increase bound with exponent r gives one with any exponent r' ≥ r: gnorm is bounded below by (Fintype.card n)⁻¹ > 0, so enlarging the exponent costs only the constant factor (Fintype.card n) ^ (r' - r).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nonempty, Matrix.GeneralLinearGroup, Real, Complex, Nat, LE.le, Norm.norm, HMul.hMul, HPow.hPow, Matrix.GeneralLinearGroup.gnorm, Exists
Proof uses: LT.lt, OfNat.ofNat, Fintype.card, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Fintype.card_pos, Iff.mp, Matrix, mul_nonneg_iff_of_pos_right, pow_pos, Matrix.GeneralLinearGroup.gnorm_pos, LE.le.trans, norm_nonneg, Eq, HAdd.hAdd, Nat.exists_eq_add_of_le and 41 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma exists_forall_norm_le_pow_of_le [Nonempty n] {φ : GL n ℝ → ℂ} {C : ℝ} {r : ℕ}
    (h : ∀ y, ‖φ y‖ ≤ C * gnorm y ^ r) {r' : ℕ} (hr : r ≤ r') :
    ∃ C', ∀ y, ‖φ y‖ ≤ C' * gnorm y ^ r' := by
…
```
Mentions: Matrix.GeneralLinearGroup.gnorm
lemma Matrix.GeneralLinearGroup.IsSlowlyIncreasing.add line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup, Real, Complex, Matrix.GeneralLinearGroup.IsSlowlyIncreasing, HAdd.hAdd
Proof uses: Exists, Nat, LE.le, Norm.norm, HMul.hMul, HPow.hPow, Matrix.GeneralLinearGroup.gnorm, IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Subsingleton, Subsingleton.intro, Units.ext, Matrix, Subsingleton.elim, Matrix.GeneralLinearGroup.IsSlowlyIncreasing.of_bounded, OfNat.ofNat, norm_add_le, Eq.symm and 9 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.isZFinite_oneSmoothGL The constant function 1 is Z(𝔤)-finite: the kernel of constantsCharacter is an ideal of finite codimension annihilating it line 350 source
Source documentation
The constant function 1 is Z(𝔤)-finite: the kernel of constantsCharacter is an ideal of finite codimension annihilating it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, AutomorphicForm.IsZFinite, Complex, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL, Matrix.GeneralLinearGroup.oneSmoothGL
Proof uses: AutomorphicForm.IsZFinite.of_forall_smul_eq_algHom_smul, Matrix.GeneralLinearGroup.constantsCharacter, Matrix.GeneralLinearGroup.eq_smul_oneSmoothGL_of_mem_span, HSMul.hSMul, Matrix.GeneralLinearGroup.smul_oneSmoothGL_mem_span
69 instances, coercions and auxiliary constants left out.
```
lemma isZFinite_oneSmoothGL :
    IsZFinite ℂ ↥(centerUniversalEnveloping n) (oneSmoothGL n) :=
…
```
Mentions: Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup.oneSmoothGL
lemma Matrix.GeneralLinearGroup.isZFinite_const_smoothGL Every constant function is Z(𝔤)-finite line 356 source
Source documentation
Every constant function is Z(𝔤)-finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Complex, AutomorphicForm.IsZFinite, Subtype, Matrix.GeneralLinearGroup.universalEnveloping, Membership.mem, Subalgebra, Matrix, LieRing.ofAssociativeRing, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup, Real, Submodule, Matrix.GeneralLinearGroup.smoothGL, Subtype.mk, Matrix.GeneralLinearGroup.isSmoothOnGL_const
Proof uses: Eq.rec, HSMul.hSMul, Matrix.GeneralLinearGroup.oneSmoothGL, Eq, AutomorphicForm.IsZFinite.const_smul, Matrix.GeneralLinearGroup.isZFinite_oneSmoothGL, Subtype.ext, funext, mul_one
73 instances, coercions and auxiliary constants left out.
```
lemma isZFinite_const_smoothGL (c : ℂ) :
    IsZFinite ℂ ↥(centerUniversalEnveloping n)
      (⟨fun _ => c, isSmoothOnGL_const c⟩ : smoothGL n) :=
…
```
Mentions: c, Matrix.GeneralLinearGroup.centerUniversalEnveloping, Matrix.GeneralLinearGroup.isSmoothOnGL_const, Matrix.GeneralLinearGroup.smoothGL
structure Matrix.GeneralLinearGroup.IsSmoothAdelic Smoothness of a function on G(𝔸) = G(𝔸_f) × G(ℝ), with G(𝔸_f) = GL n 𝔸ᶠ[ℤ, ℚ]: continuous, locally constant in the finite variable, and C^∞ in the archimedean variable line 366 source
Source documentation
Smoothness of a function on G(𝔸) = G(𝔸_f) × G(ℝ), with G(𝔸_f) = GL n 𝔸ᶠ[ℤ, ℚ]: continuous, locally constant in the finite variable, and C^∞ in the archimedean variable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex
14 instances, coercions and auxiliary constants left out.
```
structure IsSmoothAdelic (f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) : Prop where
…
```
structure Matrix.GeneralLinearGroup.IsAutomorphicForm Documented declaration: IsAutomorphicForm line 377 source
Source documentation
An automorphic form for (G, K) in the sense of Borel-Jacquet, with G = GL n / ℚ and K = O n ℝ: G(𝔸) is written as G(𝔸_f) × G(ℝ) = GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ, condition (a) is invariance under ratDiagonal n, the rational points embedded diagonally, condition (b2) is finiteness under the maximal compact orthogonalSubgroup n, and condition (c) is with respect to the action of the centre of the universal enveloping algebra by left invariant differential operators, centerAction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex
14 instances, coercions and auxiliary constants left out.
```
structure IsAutomorphicForm (f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) : Prop where
…
```
lemma Matrix.GeneralLinearGroup.isSmoothAdelic_const line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Complex, Matrix.GeneralLinearGroup.IsSmoothAdelic, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real
Proof uses: Matrix.GeneralLinearGroup.IsSmoothAdelic.mk, continuous_const, Matrix, IsLocallyConstant.const, Matrix.GeneralLinearGroup.isSmoothOnGL_const
42 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.IsSmoothAdelic.add line 404 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothAdelic, HAdd.hAdd
Proof uses: Matrix.GeneralLinearGroup.IsSmoothAdelic.mk, Continuous.add, Matrix, Matrix.GeneralLinearGroup.IsSmoothAdelic.continuous, IsLocallyConstant.add, Prod.mk, Matrix.GeneralLinearGroup.IsSmoothAdelic.locallyConstant, Matrix.GeneralLinearGroup.IsSmoothOnGL.add, Matrix.GeneralLinearGroup.IsSmoothAdelic.smoothOnGL
60 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.IsSmoothAdelic.const_smul line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex, Matrix.GeneralLinearGroup.IsSmoothAdelic, HSMul.hSMul
Proof uses: Matrix.GeneralLinearGroup.IsSmoothAdelic.mk, Continuous.const_smul, Matrix, Matrix.GeneralLinearGroup.IsSmoothAdelic.continuous, IsLocallyConstant.comp, Prod.mk, Matrix.GeneralLinearGroup.IsSmoothAdelic.locallyConstant, Matrix.GeneralLinearGroup.IsSmoothOnGL.const_smul, Matrix.GeneralLinearGroup.IsSmoothAdelic.smoothOnGL
63 instances, coercions and auxiliary constants left out.
theorem Matrix.GeneralLinearGroup.isAutomorphicForm_const Sanity check: the constant functions are automorphic forms line 420 source
Source documentation
Sanity check: the constant functions are automorphic forms. This exercises every condition of the definition: condition (b1) is witnessed by the compact open subgroup integralAdelicSubgroup n and condition (c) by the kernel of constantsCharacter n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Complex, Matrix.GeneralLinearGroup.IsAutomorphicForm, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real
Proof uses: Matrix.GeneralLinearGroup.IsAutomorphicForm.mk, Matrix.GeneralLinearGroup.isSmoothAdelic_const, Membership.mem, Subgroup, Matrix, Matrix.GeneralLinearGroup.ratDiagonal, rfl, Exists.intro, And, IsOpen, IsCompact, Eq, Matrix.GeneralLinearGroup.integralAdelicSubgroup, And.intro, Matrix.GeneralLinearGroup.isOpen_integralAdelicSubgroup, Matrix.GeneralLinearGroup.isCompact_integralAdelicSubgroup, AutomorphicForm.isKFinite_of_rightInvariant, Subgroup.prod, Bot.bot, Matrix.GeneralLinearGroup.orthogonalSubgroup and 12 more
63 instances, coercions and auxiliary constants left out.
```
theorem isAutomorphicForm_const (c : ℂ) :
    IsAutomorphicForm (fun _ : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ => c) where
…
```
Mentions: c, Matrix.GeneralLinearGroup.IsAutomorphicForm
theorem Matrix.GeneralLinearGroup.isAutomorphicForm_one Sanity check: the constant function 1 is an automorphic form line 432 source
Source documentation
Sanity check: the constant function 1 is an automorphic form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Matrix.GeneralLinearGroup.IsAutomorphicForm, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, OfNat.ofNat, Complex
Proof uses: Matrix.GeneralLinearGroup.isAutomorphicForm_const
18 instances, coercions and auxiliary constants left out.
```
theorem isAutomorphicForm_one :
    IsAutomorphicForm (fun _ : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ => (1 : ℂ)) :=
…
```
Mentions: Matrix.GeneralLinearGroup.IsAutomorphicForm
lemma Matrix.GeneralLinearGroup.IsAutomorphicForm.add line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex, Matrix.GeneralLinearGroup.IsAutomorphicForm, HAdd.hAdd
Proof uses: Matrix.GeneralLinearGroup.IsAutomorphicForm.mk, Matrix.GeneralLinearGroup.IsSmoothAdelic.add, Matrix.GeneralLinearGroup.IsAutomorphicForm.smooth, Membership.mem, Subgroup, Matrix, Matrix.GeneralLinearGroup.ratDiagonal, of_eq_true, Eq, HMul.hMul, Eq.trans, True, congrFun', congrArg, congr, Matrix.GeneralLinearGroup.IsAutomorphicForm.left_invariant, eq_self, Exists, And, IsOpen and 38 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Matrix.GeneralLinearGroup.IsAutomorphicForm.const_smul line 450 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex, Matrix.GeneralLinearGroup.IsAutomorphicForm, HSMul.hSMul
Proof uses: Matrix.GeneralLinearGroup.IsAutomorphicForm.mk, Matrix.GeneralLinearGroup.IsSmoothAdelic.const_smul, Matrix.GeneralLinearGroup.IsAutomorphicForm.smooth, Membership.mem, Subgroup, Matrix, Matrix.GeneralLinearGroup.ratDiagonal, of_eq_true, Eq, HMul.hMul, Eq.trans, True, congrFun', congrArg, Matrix.GeneralLinearGroup.IsAutomorphicForm.left_invariant, eq_self, And, IsOpen, IsCompact, Prod.mk and 24 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Matrix.GeneralLinearGroup.automorphicForms The automorphic forms for GL n / ℚ as a ℂ-submodule of the functions on G(𝔸) line 463 source
Source documentation
The automorphic forms for GL n / ℚ as a ℂ-submodule of the functions on G(𝔸).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Submodule, Complex, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real
Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, Matrix.GeneralLinearGroup.IsAutomorphicForm, Membership.mem, Set, Matrix.GeneralLinearGroup.IsAutomorphicForm.add, Matrix.GeneralLinearGroup.IsAutomorphicForm.const_smul
41 instances, coercions and auxiliary constants left out.
```
def automorphicForms : Submodule ℂ (GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ) where
…
```
lemma Matrix.GeneralLinearGroup.mem_automorphicForms line 470 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex, Iff, Membership.mem, Submodule, Matrix.GeneralLinearGroup.automorphicForms, Matrix.GeneralLinearGroup.IsAutomorphicForm
Proof uses: Iff.rfl
42 instances, coercions and auxiliary constants left out.
lemma Matrix.GeneralLinearGroup.IsAutomorphicForm.rightTranslate Automorphy is preserved by right translation in the finite variable line 474 source
Source documentation
Automorphy is preserved by right translation in the finite variable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Prod, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, Real, Complex, Matrix.GeneralLinearGroup.IsAutomorphicForm, Prod.mk, HMul.hMul, Matrix, Prod.fst, Prod.snd
Proof uses: Matrix.GeneralLinearGroup.IsAutomorphicForm.mk, Matrix.GeneralLinearGroup.IsSmoothAdelic.mk, Continuous.comp, Matrix.GeneralLinearGroup.IsSmoothAdelic.continuous, Matrix.GeneralLinearGroup.IsAutomorphicForm.smooth, Continuous.prodMk, Continuous.mul, continuous_fst, continuous_const, continuous_snd, IsLocallyConstant.comp_continuous, Matrix.GeneralLinearGroup.IsSmoothAdelic.locallyConstant, continuous_mul_const, Matrix.GeneralLinearGroup.IsSmoothAdelic.smoothOnGL, Membership.mem, Subgroup, Matrix.GeneralLinearGroup.ratDiagonal, Eq.mpr, Eq, id and 77 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
protected lemma IsAutomorphicForm.rightTranslate {f : GL n 𝔸ᶠ[ℤ, ℚ] × GL n ℝ → ℂ}
    (hf : IsAutomorphicForm f) (g : GL n 𝔸ᶠ[ℤ, ℚ]) :
    IsAutomorphicForm (fun p => f (p.1 * g, p.2)) where
…
```
Mentions: Matrix.GeneralLinearGroup.IsAutomorphicForm
def Matrix.GeneralLinearGroup.rightTranslation The right translation representation of G(𝔸_f) on the automorphic forms: g acts by f ↦ fun (x, y) => f (x * g, y) line 508 source
Source documentation
The right translation representation of G(𝔸_f) on the automorphic forms: g acts by f ↦ fun (x, y) => f (x * g, y).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, MonoidHom, Matrix.GeneralLinearGroup, IsDedekindDomain.FiniteAdeleRing, Int, Rat, LinearMap, Complex, RingHom.id, Subtype, Prod, Real, Membership.mem, Submodule, Matrix.GeneralLinearGroup.automorphicForms, Matrix
Proof uses: MonoidHom.mk, OneHom.mk, LinearMap.mk, AddHom.mk, Subtype.mk, Prod.mk, HMul.hMul, Prod.fst, Prod.snd
71 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def rightTranslation :
    GL n 𝔸ᶠ[ℤ, ℚ] →* (automorphicForms n →ₗ[ℂ] automorphicForms n) where
…
```
Mentions: Matrix.GeneralLinearGroup.automorphicForms