← all areas

Namespace TraceFibrePushforward 5 theorems

• Trace push-forward of factorisable adelic test functions TraceFibrePushforward.exists_forall_tracePushforward_eq_indicator_of_forall_eq_indicator 2 below · cited by 4 · depth 28
• Adelic integration factors through the trace fibration, up to a constant TraceFibrePushforward.exists_forall_lintegral_eq_mul_lintegral_lintegral_traceFibre 2 below · cited by 2 · depth 30
• Dilation law for trace fibres and the trace push-forward TraceFibrePushforward.lintegral_traceFibre_mul_and_tracePushforward_mul 0 below · cited by 2 · depth 32
• Trace push-forward of smooth-by-locally-constant tensors is Schwartz–Bruhat TraceFibrePushforward.tracePushforward_mem_schwartzBruhat 2 below · cited by 1 · depth 32
• Fundamental-domain lattice sums of σ-1 via the trace fibration TraceFibrePushforward.setLIntegral_tsum_actSubId_eq_mul_measure_mul_tsum 2 below · cited by 1 · depth 33