← all areas

Namespace HaarQuotient 20 theorems

• Bruhat density integrates to one over each coset HaarQuotient.lintegral_density_mul_eq_one 0 below · cited by 39 · depth 18
• Unfolding a left invariant measure along a closed unimodular subgroup HaarQuotient.lintegral_eq_lintegral_lintegral_mul_out 0 below · cited by 48 · depth 18
• Complex shell-peeling identity for integrals over Hbackslash G HaarQuotient.integrable_and_integral_mul_comp_out_eq_tsum_mul_setIntegral_of_mem_normalizer 5 below · cited by 1 · depth 20
• Bochner quotient integral formula over a fundamental domain HaarQuotient.integrable_setIntegral_mul_out_and_setIntegral_eq_integral_setIntegral_mul_out 1 below · cited by 18 · depth 20
• Measure of H· K for the pinned orbit density HaarQuotient.lintegral_indicator_coe_mul_coe_withDensity_density_eq_div_and_lt_top 3 below · cited by 6 · depth 20
• Pushforward of a density with constant coset integral HaarQuotient.map_mk_withDensity_eq_smul_measure 2 below · cited by 9 · depth 20
• Quotient integration formula over fundamental domains for Γ ≤ H ≤ G HaarQuotient.setLIntegral_eq_lintegral_setLIntegral_mul_out 0 below · cited by 7 · depth 20
• Right translation scales H-invariant Bochner integrals HaarQuotient.exists_forall_integrable_comp_mul_right_iff_and_integral_eq_smul 4 below · cited by 8 · depth 21
• Rescaling of quotient integrals under change of Haar normalisations HaarQuotient.exists_forall_integral_withDensity_density_eq_smul_of_isHaarMeasure 3 below · cited by 2 · depth 21
• Relative invariance of the quotient measure under the normaliser HaarQuotient.lintegral_comp_inv_mul_out_eq_mul_lintegral_of_mem_normalizer 2 below · cited by 3 · depth 21
• Peeling a ℤ-index off a quotient integral over Hbackslash G HaarQuotient.lintegral_mul_comp_out_eq_tsum_zpow_mul_setLIntegral_of_mem_normalizer 4 below · cited by 1 · depth 21
• Right translation scales the density-weighted Haar integral HaarQuotient.exists_lintegral_comp_mul_right_withDensity_density_eq_mul 3 below · cited by 2 · depth 22
• Right translation invariance of the density-weighted integral HaarQuotient.lintegral_density_mul_comp_mul_right_eq_of_map_mul_right_eq 3 below · cited by 4 · depth 23
• Measurability of orbit integrals on the coset space H backslash G HaarQuotient.measurable_lintegral_mul_out 0 below · cited by 8 · depth 23
• Integral over a double coset HtK against a quotient density HaarQuotient.setLIntegral_withDensity_eq_inv_mul_setLIntegral_of_forall_lintegral_eq 0 below · cited by 1 · depth 23
• Finiteness of H· K for the Haar cut-off measure HaarQuotient.withDensity_density_coe_mul_lt_top_of_isCompact 6 below · cited by 1 · depth 27
• Involutive automorphism preserving H fixes the quotient integral HaarQuotient.integral_comp_mulEquiv_withDensity_density_eq_of_involutive 3 below · cited by 2 · depth 28
• Right translations preserving μ preserve quotient integrals on Hbackslash G HaarQuotient.lintegral_comp_out_mul_eq_of_map_mul_right_eq 4 below · cited by 4 · depth 31
• Compact sets have finite Haar quotient measure HaarQuotient.measure_image_mk_lt_top_and_withDensity_density_coe_mul_lt_top_of_isCompact 1 below · cited by 3 · depth 31
• Quotient integral formula for complex integrable functions HaarQuotient.integrable_integral_comp_mul_out_and_integral_eq_integral_integral_comp_mul_out 1 below · cited by 6 · depth 34