← all areas

Namespace EisensteinGeneral 25 theorems

Arch 3 · Factorization 3 · Glue 3 · LocalCorrection 2 · LocalRam 3 · LocalUnr 3 · Piece 7 · Unfolding 1

EisensteinGeneral.Arch 3

• Entire continuation and exponential decay of the complex K-type integral EisensteinGeneral.Arch.exists_complexKType 1 below · cited by 4 · depth 22
• Entire continuation and decay of the real K-type integral EisensteinGeneral.Arch.exists_realKType 1 below · cited by 4 · depth 22
• Uniform exponential bound for a K-Bessel archimedean integral EisensteinGeneral.Arch.exists_norm_archIntegral_le 0 below · cited by 2 · depth 23

EisensteinGeneral.Factorization 3

• Box-normalised Fourier integral of a pure tensor factors EisensteinGeneral.Factorization.inv_measure_adelicBox_mul_fourierIntegral_tensor_eq 2 below · cited by 9 · depth 18
• Finite-level factorisation of an adelic integral into local integrals EisensteinGeneral.Factorization.inv_measure_mul_setIntegral_integralOffSet_finprod_eq 0 below · cited by 3 · depth 19
• Factorisation of an adelic integral into local integrals EisensteinGeneral.Factorization.integrable_finprod_and_inv_measure_mul_integral_eq_tprod 0 below · cited by 13 · depth 21

EisensteinGeneral.Glue 3

• Integrability of split functions on the adele ring EisensteinGeneral.Glue.integrable_mul_of_integrable_of_integrable 1 below · cited by 12 · depth 21
• Linearity of the Whittaker coefficient of a Bruhat series EisensteinGeneral.Glue.whittakerCoefficient_bruhatSeries_eq_finset_sum 1 below · cited by 1 · depth 21
• Whittaker integrability and almost-everywhere summability of Bruhat series EisensteinGeneral.Glue.whittakerCoefficientIntegrable_bruhatSeries_and_ae_summable_of_integrable 0 below · cited by 1 · depth 22

EisensteinGeneral.LocalCorrection 2

• Uniform half-plane bound for the local correction factor EisensteinGeneral.LocalCorrection.exists_forall_norm_corrOn_le_of_le_re 0 below · cited by 1 · depth 35
• Half-plane bound for the local correction factor corrOff EisensteinGeneral.LocalCorrection.norm_corrOff_le_of_le_re 0 below · cited by 1 · depth 35

EisensteinGeneral.LocalRam 3

• Integrability of the twisted smooth local integrand at a finite place EisensteinGeneral.LocalRam.integrable_twisted_smooth 2 below · cited by 9 · depth 21
• Shell expansion of a twisted local smooth integral EisensteinGeneral.LocalRam.integral_twisted_smooth_eq 2 below · cited by 4 · depth 22
• Vanishing of a twisted local integral at large frequency EisensteinGeneral.LocalRam.integral_twisted_smooth_eq_zero_of_exp_lt 1 below · cited by 4 · depth 22

EisensteinGeneral.LocalUnr 3

• Twisted unramified intertwining integrand: integrability and L¹ norm EisensteinGeneral.LocalUnr.integrable_twisted_and_integral_norm_eq 1 below · cited by 8 · depth 21
• Twisted unramified intertwining integral as a finite geometric sum EisensteinGeneral.LocalUnr.integral_twisted_eq 4 below · cited by 4 · depth 22
• Vanishing of the twisted unramified local integral off level n EisensteinGeneral.LocalUnr.integral_twisted_eq_zero_of_exp_lt 1 below · cited by 4 · depth 22

EisensteinGeneral.Piece 7

• Continuity of the inducing characters of a non-vanishing section EisensteinGeneral.Piece.continuous_and_continuous_of_isInducedSection_of_continuous_of_ne_zero 0 below · cited by 2 · depth 21
• Whittaker coefficients: partial Euler product times entire family EisensteinGeneral.Piece.exists_entire_partialEulerProduct_mul_eq_whittakerCoefficient_and_summable_majorant 25 below · cited by 1 · depth 21
• Factorisation data exist for flat nonzero induced families EisensteinGeneral.Piece.exists_forall_nonempty_factorizationDatum 9 below · cited by 5 · depth 21
• Adelic integrability of big-cell values for Re s>1 EisensteinGeneral.Piece.integrable_weyl_unipotent_mul_of_factorization 9 below · cited by 5 · depth 21
• Affine change of variables in a twisted adelic integral EisensteinGeneral.Piece.integral_smul_add_mul_addChar_neg_mul_eq 0 below · cited by 6 · depth 21
• Summable majorant for Eisenstein coefficient pieces EisensteinGeneral.Piece.exists_summable_majorant_of_lattice_vanishing 0 below · cited by 1 · depth 22
• Uniform factorisation datum at the identity for flat Eisenstein pieces EisensteinGeneral.Piece.exists_forall_exists_factorizationDatum_one_uniform_of_flat_principalLevel_archCutSubmodule 38 below · cited by 1 · depth 35

EisensteinGeneral.Unfolding 1

• Unfolding the Whittaker coefficient of a Bruhat-form Eisenstein series EisensteinGeneral.Unfolding.whittakerCoefficient_bruhatSeries_eq_of_isInducedSection 1 below · cited by 4 · depth 22