← all areas

Namespace MeasureTheory 132 theorems

— 104 · IsFundamentalDomain 3 · L2 3 · Lp 1 · Measure 21

directly in MeasureTheory 104

• Integral over a compact group as a finite coset average MeasureTheory.exists_integral_eq_inv_card_mul_sum_of_isOpen_subgroup 0 below · cited by 4 · depth 19
• Locally constant cut-off with unit T-integral on TΩ MeasureTheory.exists_isLocallyConstant_integral_subgroup_mul_eq_one 0 below · cited by 10 · depth 19
• Holomorphy of a locally dominated parametric integral MeasureTheory.differentiableOn_integral_of_forall_differentiableOn_of_locally_norm_le 0 below · cited by 6 · depth 20
• Godement's finite-dimensionality lemma on a finite-measure window MeasureTheory.finiteDimensional_and_finrank_le_of_forall_norm_le_mul_eLpNorm_restrict 1 below · cited by 1 · depth 20
• Independence of weighted integrals from the choice of cut-off function MeasureTheory.integral_mul_eq_integral_mul_of_integral_subgroup_translate_eq_one 0 below · cited by 13 · depth 20
• Jensen-type L² bound for averages against a probability density MeasureTheory.lintegral_enorm_sub_integral_mul_sq_le_lintegral_mul_lintegral_enorm_sub_sq 0 below · cited by 3 · depth 20
• Finite unions of right translates have finite measure MeasureTheory.measure_biUnion_finset_image_mul_right_lt_top 0 below · cited by 1 · depth 20
• Holomorphy and real positivity of dominated parameter integrals MeasureTheory.analyticOnNhd_integral_and_im_eq_zero_and_re_pos_of_locally_norm_le_of_re_pos_at 1 below · cited by 1 · depth 21
• Arzelà–Ascoli in Lᵖ: finite ε-nets for equicontinuous families MeasureTheory.exists_finset_forall_exists_eLpNorm_sub_lt_of_equicontinuous_of_forall_ae_norm_le 0 below · cited by 1 · depth 21
• Pratt's lemma for lower integrals with moving dominators MeasureTheory.tendsto_lintegral_nhds_zero_of_le_of_limsup_lintegral_le 0 below · cited by 1 · depth 21
• Continuous idempotent weight projecting onto ρ-isotypic vectors MeasureTheory.exists_continuous_convolution_self_eq_forall_integral_smul_isotypic 0 below · cited by 1 · depth 22
• Continuous cut-off with T-orbit integral one on a compact set MeasureTheory.exists_continuous_integral_subgroup_mul_eq_one 0 below · cited by 1 · depth 22
• Peeling a geometric shell index off a lower Lebesgue integral MeasureTheory.lintegral_mul_comp_eq_tsum_zpow_mul_setLIntegral_of_measure_image_eq_mul 0 below · cited by 1 · depth 22
• Non-vanishing matrix coefficient mean for isometric representations MeasureTheory.exists_integral_conj_apply_smul_ne_zero_of_forall_norm_apply_eq_of_continuous 1 below · cited by 1 · depth 23
• Harnack chain: iterated sub-mean-value and overlap bound MeasureTheory.exists_mem_le_of_setAverage_chain 1 below · cited by 1 · depth 23
• Integrating out θ over the Iwasawa region MeasureTheory.setIntegral_iwasawaRegion_eq_two_pi_mul_of_theta_free 0 below · cited by 16 · depth 23
• Point selection from a set average on a large subset MeasureTheory.exists_div_le_of_le_setAverage_of_nonpos 0 below · cited by 1 · depth 24
• Bruhat section functions for a closed subgroup MeasureTheory.exists_hasCompactSupport_integral_subgroup_translate_eq_one_of_subset_mul 0 below · cited by 10 · depth 24
• Fibrewise functional equation transported through an outer integral MeasureTheory.exists_hasSum_mul_zpow_eval_mul_integral_prod_of_ae_forall_integral_mul_zpow_mul_eval_eq 3 below · cited by 2 · depth 24
• Non-vanishing Fourier coefficient of a locally continuous integrable function MeasureTheory.exists_integral_fourierChar_bilinForm_mul_ne_zero_of_continuousOn 3 below · cited by 1 · depth 24
• Besicovitch propagation of a hitting bound from small balls MeasureTheory.measure_setOf_exists_mem_le_mul_of_forall_closedBall 0 below · cited by 1 · depth 24
• Analyticity and positivity of a two-sided Mellin transform MeasureTheory.analyticOnNhd_integral_mul_abs_cpow_sub_two_of_forall_integrable 0 below · cited by 1 · depth 25
• Entirety, joint continuity and strip bounds for N^s-integrals MeasureTheory.differentiable_and_continuous_integral_mul_cpow_of_eventually_norm_mul_rpow_add_rpow_neg_le 0 below · cited by 4 · depth 25
• Shell decomposition of an integral with integer exponent MeasureTheory.hasSum_setIntegral_preimage_mul_zpow_of_integrable_mul_zpow 0 below · cited by 2 · depth 25
• Laurent coefficients of a functional equation on an annulus MeasureTheory.sum_coeff_mul_setIntegral_preimage_eq_of_forall_integral_mul_zpow_mul_eval_eq 2 below · cited by 1 · depth 25
• Borel transversal for a discrete subgroup MeasureTheory.exists_measurableSet_isFundamentalDomain_op_of_discreteTopology 0 below · cited by 13 · depth 26
• Independence of int f d(ρμ) from the normalised density ρ MeasureTheory.integrable_and_integral_withDensity_eq_of_forall_lintegral_subgroup_mul_eq_one 0 below · cited by 1 · depth 26
• Independence of the normalising density for H-invariant integrands MeasureTheory.lintegral_mul_eq_lintegral_mul_of_forall_lintegral_subgroup_mul_eq_one 0 below · cited by 1 · depth 26
• Möbius change of variables on ℝ MeasureTheory.integral_abs_det_div_sq_mul_comp_moebius_real 0 below · cited by 1 · depth 27
• Möbius change of variables on ℂ MeasureTheory.integral_normSq_det_div_mul_comp_moebius_complex 0 below · cited by 1 · depth 27
• Countable sums through iterated integrals, L¹-summable case MeasureTheory.integral_tsum_integral_eq_tsum_integral_integral_of_summable_integral_norm 0 below · cited by 1 · depth 27
• Dirichlet localisation: int h(t)sin(Rt)/t → π h(0) MeasureTheory.tendsto_integral_sin_mul_div_mul_of_integrable_fourierIntegral 0 below · cited by 1 · depth 27
• Atom-free functional on Tᵈ with prescribed Fourier values MeasureTheory.exists_clm_torus_noAtomicMass_forall_apply_fourier_eq_prod_erase_ite_mul_one_add_neg_one_pow 0 below · cited by 1 · depth 28
• Haar functional on Tᵈ: box-small, Fourier values δ_{n,0} MeasureTheory.exists_clm_torus_noAtomicMass_forall_apply_fourier_eq_prod_ite_eq_zero 0 below · cited by 1 · depth 28
• Truncation function with unit fibre integral along ι(H) MeasureTheory.exists_continuous_hasCompactSupport_forall_integral_comp_mul_eq_one 0 below · cited by 7 · depth 28
• Winding measures with sublattice-uniform total variation bound MeasureTheory.exists_forall_exists_clm_opNorm_le_noAtomicMass_forall_hasSum_fibre_mul_fourier_eq_apply_fourier_of_le_of_discrete_of_productFormula_of_fourier_decay 7 below · cited by 1 · depth 28
• Laplace concentration: off-window tail bound from a gap MeasureTheory.setIntegral_exp_mul_le_exp_neg_mul_setIntegral_of_gap 0 below · cited by 2 · depth 28
• Automorphism stabilising a lattice has Haar character one MeasureTheory.addEquivAddHaarChar_eq_one_and_measurePreserving_of_isAddFundamentalDomain_of_forall_apply_mem_iff 0 below · cited by 2 · depth 29
• Kernels vanishing on rectangles in an exhaustion vanish a.e. MeasureTheory.ae_prod_eq_zero_of_forall_setIntegral_prod_eq_zero_of_iUnion 0 below · cited by 1 · depth 29
• A winding functional on Tᵈ: norm, no atoms, Fourier values MeasureTheory.exists_clm_opNorm_le_noAtomicMass_apply_eq_tsum_integral_mul_fourier_of_summable_of_ae_measure_fibre_eq_zero 0 below · cited by 1 · depth 29
• Uniform lattice-sum bound for a skew product Poisson kernel MeasureTheory.exists_forall_summable_integral_prod_inv_one_add_abs_sq_continuousLinearEquiv_le 0 below · cited by 1 · depth 29
• Fujisaki compactness in an abstract topological ring MeasureTheory.exists_isCompact_forall_exists_eq_mul_of_map_mul_eq_of_isAddFundamentalDomain 0 below · cited by 1 · depth 29
• Partial Poisson summation in the first a variables MeasureTheory.hasSum_translate_intCast_fst_eq_tsum_integral_fourierIntegral_of_summable 1 below · cited by 1 · depth 29
• Non-stationary phase bound for oscillatory integrals on ℝ MeasureTheory.norm_integral_mul_cexp_le_two_pow_mul_rpow_neg_of_contDiff_of_hasCompactSupport 0 below · cited by 2 · depth 29
• Integrability transfers under the substitution (u,v)↦(-u/t, u/v) MeasureTheory.integrable_mul_comp_neg_div_div_of_integrable_prod_Iio_prod_Ioi 0 below · cited by 1 · depth 30
• Reversal of a triple iterated Bochner integral MeasureTheory.integral_integral_integral_comm_of_integrable_prod_prod 0 below · cited by 1 · depth 30
• Fibre substitution (y₁,y₂)=(-u/t, u/v) for iterated integrals MeasureTheory.setIntegral_Iio_setIntegral_Ioi_eq_setIntegral_setIntegral_mul_comp_neg_div_div 0 below · cited by 1 · depth 30
• Wedge substitution t=u(σ-u), u=v/w for iterated integrals MeasureTheory.setIntegral_Ioi_setIntegral_Ioi_eq_setIntegral_setIntegral_Ioi_div_wedgeSubst 0 below · cited by 1 · depth 30
• Zero sets of non-zero real polynomials are Lebesgue-null MeasureTheory.volume_setOf_mvPolynomial_eval_eq_zero 0 below · cited by 2 · depth 30
• Coordinate domination by an L²-norm of a definite family MeasureTheory.exists_forall_norm_sq_le_mul_integral_norm_sq_sum_of_definite 0 below · cited by 1 · depth 31
• Local lower bound for change of variables at a nondegenerate point MeasureTheory.exists_isOpen_injOn_forall_mul_lintegral_comp_le_lintegral_image_of_det_fderiv_ne_zero 0 below · cited by 1 · depth 31
• A compactly supported T-section over a compact set MeasureTheory.exists_nonneg_hasCompactSupport_forall_integral_subgroup_translate_eq_one_of_isCompact 0 below · cited by 2 · depth 31
• Covolume of a cocompact closed subgroup via section functions MeasureTheory.exists_pos_forall_integral_eq_of_forall_integral_subgroup_translate_eq_one_of_isCompact 2 below · cited by 1 · depth 31
• Integrability of a bounded T-invariant function times a cut-off MeasureTheory.integrable_mul_of_integral_subgroup_translate_eq_one 0 below · cited by 2 · depth 31
• Unfolding Sbackslash G through Tbackslash G with section functions MeasureTheory.integral_mul_eq_integral_integral_subgroup_mul_mul_of_forall_integral_translate_eq_one 1 below · cited by 1 · depth 31
• L² mean value inequality along the imaginary axis MeasureTheory.integral_norm_sq_axis_sub_le_of_analyticOnNhd_of_forall_integral_norm_sq_deriv_le 0 below · cited by 2 · depth 31
• Dominated convergence for integrals against a compactly supported weight MeasureTheory.tendsto_integral_mul_nhdsGT_of_tendstoUniformlyOn_tsupport 0 below · cited by 1 · depth 31
• Measurability of characters in a measurable linear combination MeasureTheory.aestronglyMeasurable_of_aestronglyMeasurable_sum_smul_monoidHom 0 below · cited by 1 · depth 32
• Smoothness of a parametric integral of a smooth compactly supported kernel MeasureTheory.contDiff_integral_smul_comp_of_contDiff_of_hasCompactSupport 0 below · cited by 16 · depth 32
• Bruhat function for a cocompact closed subgroup MeasureTheory.exists_continuous_hasCompactSupport_forall_integral_subgroup_mul_eq_one_of_isInvInvariant 0 below · cited by 1 · depth 32
• Smooth compactly supported functions have product quadratic Fourier decay MeasureTheory.exists_forall_norm_le_mul_prod_and_norm_integral_cexp_mul_le_of_contDiff_of_hasCompactSupport 0 below · cited by 2 · depth 32
• Summable angular Fourier modes of a smooth periodic window MeasureTheory.exists_summable_forall_norm_setIntegral_mul_cexp_le_prod_of_contDiff_of_periodic 3 below · cited by 4 · depth 32
• Pointwise Fourier inversion on ℝᶜ for periodic continuous functions MeasureTheory.hasSum_fourierCoeff_pi_mul_cexp_of_continuous_of_periodic_of_summable 0 below · cited by 4 · depth 32
• Mass of an indefinite quadratic shell in ℝ⁴ MeasureTheory.lintegral_inv_sq_quadForm_shell_eq 0 below · cited by 1 · depth 32
• Independence of the weight function in Weil's integration formula MeasureTheory.lintegral_mul_eq_lintegral_mul_of_forall_mul_eq_of_ae_lintegral_comp_mul_eq_one 0 below · cited by 1 · depth 32
• Sup-L² bound for finite-dimensional translation-invariant spaces MeasureTheory.sq_norm_apply_mul_measureReal_le_finrank_mul_integral_sq_norm_of_forall_mul_right_mem 0 below · cited by 1 · depth 32
• Smoothness and compact support of a parametric integral MeasureTheory.contDiff_and_hasCompactSupport_integral_mul_comp_of_contDiff_of_hasCompactSupport 0 below · cited by 2 · depth 33
• Uniform decay of angular Fourier modes of a smooth periodic window MeasureTheory.exists_forall_contDiff_norm_iteratedFDeriv_setIntegral_mul_cexp_le_mul_prod_of_contDiff_of_periodic 0 below · cited by 2 · depth 33
• Existence of a section weight for finitely many T–U double cosets MeasureTheory.exists_section_integral_mul_eq_sum_div_of_forall_eq_of_forall_exists 0 below · cited by 1 · depth 33
• Weighted T-invariant integrals are independent of the section function MeasureTheory.integrable_and_integral_mul_mul_eq_of_integral_subgroup_translate_eq_one_of_continuous 2 below · cited by 10 · depth 33
• Finite Parseval identity for vector-valued L² expansions MeasureTheory.integrable_norm_sq_sum_conj_smul_and_integral_eq_sum_mul_norm_sq_of_forall_integral_mul_conj_eq 0 below · cited by 1 · depth 33
• A measure-preserving shearing change of variables on Gⁿ⁺¹ MeasureTheory.exists_measurableEquiv_measurePreserving_pi_apply_succ_eq_inv_mul_mul 0 below · cited by 3 · depth 34
• Product-Poisson bounds for Fourier modes of kink windows MeasureTheory.exists_summable_forall_fourierMode_kinkWindow_productPoisson 20 below · cited by 1 · depth 34
• Summable Fourier modes of a kink-weighted periodic window MeasureTheory.exists_summable_forall_fourierMode_absOneSubExp_mul_productPoisson_of_contDiff_of_periodic 7 below · cited by 1 · depth 35
• Summable Fourier modes of a logarithmic complex-place germ window MeasureTheory.exists_summable_forall_fourierMode_normSqLogGerm_mul_productPoisson_of_contDiff_of_periodic 10 below · cited by 1 · depth 35
• Independence of orbit integrals from the section function MeasureTheory.lintegral_enorm_mul_eq_and_integral_mul_eq_of_forall_lintegral_comp_smul_eq_one 0 below · cited by 2 · depth 35
• Uniform C² bounds for a partial Fourier transform MeasureTheory.exists_forall_contDiff_norm_iteratedDeriv_integral_cexp_mul_le_prod_of_contDiff 3 below · cited by 1 · depth 36
• Mixed partial Fourier transform: smoothness and quadratic decay MeasureTheory.exists_forall_contDiff_norm_iteratedFDeriv_integral_setIntegral_insertNth_mul_cexp_le_prod 2 below · cited by 1 · depth 36
• Decay of a mixed Fourier transform of ρ²logρ germ MeasureTheory.exists_forall_norm_integral_integral_cexp_mul_normSq_log_germ_mul_le 4 below · cited by 1 · depth 36
• An admissible mollifier kernel with smooth compactly supported Fourier inverse MeasureTheory.exists_kernel_moments_integral_eq_one_forall_exists_contDiff_hasCompactSupport_integral_mul_scaledKernel_eq_integral_mul_cexp 0 below · cited by 1 · depth 36
• L² bound for a polynomially bounded family from kernel-averaged pairings MeasureTheory.memLp_two_and_sum_integral_norm_sq_le_of_forall_norm_sum_integral_conj_scaledKernelAverage_mul_le 0 below · cited by 1 · depth 36
• Sup bound from product decay of the Fourier transform MeasureTheory.norm_le_two_pow_mul_of_forall_norm_integral_cexp_mul_le_prod 0 below · cited by 1 · depth 36
• Density in L²(ℝ) of exponential transforms of test functions MeasureTheory.exists_contDiff_hasCompactSupport_integral_normSq_sub_integral_mul_cexp_lt_of_memLp_two 0 below · cited by 1 · depth 37
• Smooth splitting of logarithmic potentials with complex offset MeasureTheory.exists_contDiff_integral_mul_log_normSq_add_normSq_eq_add_normSq_mul_log_mul_of_hasCompactSupport 6 below · cited by 2 · depth 37
• Logarithmic potential integral splits as A+|ρ|B MeasureTheory.exists_contDiff_integral_mul_log_sq_add_sq_eq_add_abs_mul_of_hasCompactSupport 9 below · cited by 3 · depth 37
• Uniform bounds for a partial Fourier transform with one free slot MeasureTheory.exists_forall_contDiff_norm_iteratedFDeriv_integral_insertNth_mul_cexp_le_mul_prod 0 below · cited by 1 · depth 37
• Uniform decay of partial angular Fourier modes, one angle free MeasureTheory.exists_forall_contDiff_norm_iteratedFDeriv_setIntegral_insertNth_mul_cexp_le_prod 0 below · cited by 1 · depth 37
• Fourier decay for a C⁴ window times a logarithmic degree-two singularity MeasureTheory.exists_forall_norm_integral_cexp_mul_mul_le_of_norm_iteratedFDeriv_le_mul_log 0 below · cited by 1 · depth 37
• Mixed Fourier decay for C⁴ functions periodic in θ MeasureTheory.exists_forall_norm_integral_integral_cexp_mul_le_of_contDiff_of_periodic 0 below · cited by 1 · depth 37
• Differentiation under the integral sign for smooth compactly supported kernels MeasureTheory.hasDerivAt_integral_prod_mk_of_contDiff_of_hasCompactSupport 0 below · cited by 1 · depth 37
• L² error bound under a shifted Bessel-bounded mixing matrix MeasureTheory.memLp_two_and_integral_sum_norm_sq_sub_le_mul_add_of_eq_mul_add_sum_conj_mul_of_bessel 0 below · cited by 1 · depth 37
• Bessel's inequality between two finite orthonormal systems MeasureTheory.sum_norm_sq_sum_conj_integral_mul_conj_mul_le_sum_norm_sq_of_orthonormal 1 below · cited by 2 · depth 37
• Smoothness of the logarithmic potential on a closed half-space MeasureTheory.contDiffOn_integral_mul_log_sq_add_sq_halfSpace 0 below · cited by 1 · depth 38
• Even reflection of a function flat on a half-space boundary MeasureTheory.contDiff_comp_abs_of_contDiffOn_halfSpace_of_iteratedFDerivWithin_eq_zero 0 below · cited by 2 · depth 38
• Parametric log-potential along a moving linear form: smooth plus ‖r‖²log‖r‖ term MeasureTheory.exists_contDiff_integral_integral_mul_log_normSq_clm_add_normSq_eq_add_normSq_mul_log_mul_of_hasCompactSupport 8 below · cited by 1 · depth 38
• Parametric logarithmic potential along a moving linear form MeasureTheory.exists_contDiff_integral_integral_mul_log_sq_linear_add_sq_eq_add_abs_mul_of_hasCompactSupport 10 below · cited by 1 · depth 38
• Smooth decomposition of a degenerating complex log potential MeasureTheory.exists_contDiff_integral_integral_mul_log_sq_one_sub_normSq_add_normSq_conj_add_conj_mul_eq_add_abs_mul_of_hasCompactSupport 12 below · cited by 1 · depth 38
• Boundary jet on a half-space realised by a smooth function MeasureTheory.exists_contDiff_iteratedFDeriv_eq_iteratedFDerivWithin_halfSpace 4 below · cited by 2 · depth 38
• Strong continuity at 1 of right translation on L²(G,μ) MeasureTheory.exists_nhds_one_forall_eLpNorm_comp_mul_sub_lt_of_memLp_two 0 below · cited by 1 · depth 38
• Bessel's inequality for a finite orthonormal family MeasureTheory.sum_norm_sq_integral_mul_conj_le_integral_norm_sq_of_orthonormal 0 below · cited by 2 · depth 38
• Taylor osculation along the boundary of a half-space MeasureTheory.exists_contDiff_forall_iteratedFDerivWithin_sub_sum_pow_smul_halfSpace_eq_zero 2 below · cited by 1 · depth 39
• Borel's lemma with smooth compactly supported parameters MeasureTheory.exists_contDiff_forall_iteratedFDeriv_sub_sum_pow_smul_eq_zero 2 below · cited by 1 · depth 39
• Parametric log integral: smooth A(p,ρ)+|ρ|B(p,ρ) decomposition MeasureTheory.exists_contDiff_integral_integral_mul_log_sq_linear_add_sq_mul_sq_eq_add_abs_mul_of_hasCompactSupport 10 below · cited by 1 · depth 39
• Weighted L² bound for a parametric integral MeasureTheory.memLp_two_integral_and_integral_norm_sq_integral_le_of_integral_norm_sq_le_of_integrable_one_add_sq_mul 0 below · cited by 1 · depth 39

MeasureTheory.IsFundamentalDomain 3

• Fundamental domain for a subgroup from coset representatives MeasureTheory.IsFundamentalDomain.iUnion_inv_smul_of_leftCosetRepresentatives 0 below · cited by 18 · depth 20
• Unfolding an integral over coset translates of a fundamental domain MeasureTheory.IsFundamentalDomain.setLIntegral_iUnion_inv_smul_eq_and_setIntegral_eq_of_leftCosetRepresentatives 0 below · cited by 13 · depth 20
• Transport of a right-translation fundamental domain along a group isomorphism MeasureTheory.IsFundamentalDomain.image_mulEquiv_op_subgroupOf 0 below · cited by 1 · depth 27

MeasureTheory.L2 3

• Convolution by a Hermitian continuous kernel is compact and symmetric MeasureTheory.L2.exists_convolutionCLM_isCompactOperator_of_compactSpace 2 below · cited by 2 · depth 18
• Convolution by a Hermitian kernel is symmetric on L²(G) MeasureTheory.L2.convolutionCLM_isSymmetric_of_conj_neg 0 below · cited by 1 · depth 19
• Convolution by a continuous function is compact on L² MeasureTheory.L2.exists_convolutionCLM_isCompactOperator 0 below · cited by 1 · depth 19

MeasureTheory.Lp 1

• Godement's finite-dimensionality lemma for subspaces of L² MeasureTheory.Lp.finiteDimensional_and_finrank_le_of_forall_ae_norm_le_mul_norm 0 below · cited by 1 · depth 21

MeasureTheory.Measure 21

• Translation-invariant measures on G× Y are μ⊗σ MeasureTheory.Measure.exists_eq_prod_of_forall_map_add_left 0 below · cited by 6 · depth 18
• Splitting a Haar measure along an isomorphism onto a product MeasureTheory.Measure.exists_isHaarMeasure_map_continuousMulEquiv_eq_prod 0 below · cited by 9 · depth 19
• Uniqueness of invariant measures on homogeneous spaces with compact stabilisers MeasureTheory.Measure.exists_eq_smul_map_smul_of_forall_map_smul_eq_of_isCompact_stabilizer 0 below · cited by 2 · depth 20
• Haar measure on GL₂(ℝ) in Iwasawa coordinates MeasureTheory.Measure.exists_isHaarMeasure_GL_two_real_eq_smul_map_iwasawa 0 below · cited by 2 · depth 20
• Haar measure on GL₂(ℝ) is (det)⁻² dA up to scalar MeasureTheory.Measure.exists_isHaarMeasure_GL_two_real_eq_smul_map_det_sq_inv 0 below · cited by 1 · depth 23
• Pushforward of Haar measure on a fundamental domain MeasureTheory.Measure.exists_map_restrict_eq_smul_restrict_range_of_isFundamentalDomain 0 below · cited by 2 · depth 25
• Unimodular Haar measure is inversion invariant MeasureTheory.Measure.isInvInvariant_of_isMulRightInvariant 0 below · cited by 17 · depth 26
• Unimodularity of groups compact modulo central elements MeasureTheory.Measure.isMulRightInvariant_of_forall_exists_eq_mul_of_isCompact 0 below · cited by 5 · depth 28
• Haar measure |χ|⁻¹ dx on units of a real subalgebra MeasureTheory.Measure.exists_isHaarMeasure_subgroup_units_map_val_eq_withDensity_of_abs_det_eq 0 below · cited by 2 · depth 29
• Haar measure of a bi-invariant group factorised as T· S MeasureTheory.Measure.exists_haar_eq_smul_map_mul_prod_of_homeomorph 0 below · cited by 1 · depth 30
• Haar pushforward along an isomorphism onto a finite product MeasureTheory.Measure.exists_ne_zero_map_mulEquiv_eq_smul_pi 0 below · cited by 2 · depth 30
• Gram-normalised measure transported by a form-preserving automorphism MeasureTheory.Measure.map_withDensity_gramMeasure_eq_of_linearEquiv_of_bilinForm_eq 0 below · cited by 2 · depth 30
• Gram-normalised trace measures on M₂ of a product algebra MeasureTheory.Measure.map_withDensity_gram_trace_matrix_pi_eq_pi_of_span_eq 3 below · cited by 1 · depth 30
• Haar factorisation for an abstract restricted product MeasureTheory.Measure.exists_haar_forall_lintegral_mul_prod_mul_indicator_eq_mul_lintegral_mul_prod_lintegral_of_restrictedProduct 0 below · cited by 2 · depth 31
• Weil's formula: pushforward of quotient Haar measure along open-range f MeasureTheory.Measure.exists_map_apply_out_haarQuotient_eq_smul_restrict_range_of_isOpen_range 5 below · cited by 2 · depth 31
• Basis independence of the Gram-normalised Lebesgue measure MeasureTheory.Measure.gram_smul_map_volume_eq_of_span_eq 0 below · cited by 4 · depth 31
• Continuous involutive automorphisms preserve Haar measure MeasureTheory.Measure.map_eq_self_of_involutive_of_isHaarMeasure 0 below · cited by 2 · depth 31
• Measure of a subgroup as relative index times measure MeasureTheory.Measure.measure_coe_eq_relIndex_mul_of_le_of_isMulLeftInvariant 0 below · cited by 1 · depth 32
• Gram measure of the trace form on matrix algebras MeasureTheory.Measure.gram_trace_matrix_smul_map_volume_eq_pow_smul_map_of_pi_pi 1 below · cited by 1 · depth 33
• Relative index scaling for a left-invariant measure MeasureTheory.Measure.measure_coe_eq_relIndex_mul_of_le_of_isAddLeftInvariant 0 below · cited by 4 · depth 34
• Gram-normalised Lebesgue measure of a parallelepiped MeasureTheory.Measure.sqrt_abs_det_gram_smul_map_volume_image_pi_Ico_eq_of_span_eq 1 below · cited by 2 · depth 35