Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 3b52265

Browse files
hrmacbethAlexKontorovich
hrmacbeth
and
AlexKontorovich
committed
feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863)
We prove the "unfolding trick": Given a subgroup `Γ` of a group `G`, the integral of a function `f` on `G` times the lift to `G` of a function `g` on the coset space `G ⧸ Γ` with respect to a right-invariant measure `μ` on `G`, is equal to the integral over the coset space of the automorphization of `f` times `g`. We also prove the following simplified version: Given a subgroup `Γ` of a group `G`, the integral of a function `f` on `G` with respect to a right-invariant measure `μ` is equal to the integral over the coset space `G ⧸ Γ` of the automorphization of `f`. A question: is it possible to deduce `ae_strongly_measurable (quotient_group.automorphize f) μ_𝓕` from `ae_strongly_measurable f μ` (as opposed to assuming it as a hypothesis in the main theorem)? It seems quite plausible... Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com> Co-authored-by: AlexKontorovich <58564076+AlexKontorovich@users.noreply.github.com>
1 parent 0c1d80f commit 3b52265

5 files changed

Lines changed: 343 additions & 8 deletions

File tree

‎src/group_theory/group_action/group.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,6 +191,17 @@ def distrib_mul_action.to_add_equiv (x : α) : β ≃+ β :=
191191
{ .. distrib_mul_action.to_add_monoid_hom β x,
192192
.. mul_action.to_perm_hom α β x }
193193

194+
/-- Each non-zero element of a `group_with_zero` defines an additive monoid isomorphism of an
195+
`add_monoid` on which it acts distributively.
196+
197+
This is a stronger version of `distrib_mul_action.to_add_monoid_hom`. -/
198+
def distrib_mul_action.to_add_equiv₀ {α : Type*} (β : Type*) [group_with_zero α] [add_monoid β]
199+
[distrib_mul_action α β] (x : α) (hx : x ≠ 0) : β ≃+ β :=
200+
{ inv_fun := λ b, x⁻¹ • b,
201+
left_inv := inv_smul_smul₀ hx,
202+
right_inv := smul_inv_smul₀ hx,
203+
.. distrib_mul_action.to_add_monoid_hom β x, }
204+
194205
variables (α β)
195206

196207
/-- Each element of the group defines an additive monoid isomorphism.

‎src/measure_theory/function/strongly_measurable/basic.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1740,6 +1740,13 @@ end
17401740

17411741
end ae_strongly_measurable
17421742

1743+
lemma ae_strongly_measurable_of_absolutely_continuous {α β : Type*} [measurable_space α]
1744+
[topological_space β] {μ ν : measure α} (h : ν ≪ μ) (g : α → β)
1745+
(hμ : ae_strongly_measurable g μ) : ae_strongly_measurable g ν :=
1746+
begin
1747+
obtain ⟨g₁, hg₁, hg₁'⟩ := hμ,
1748+
refine ⟨g₁, hg₁, h.ae_eq hg₁'⟩,
1749+
end
17431750

17441751
/-! ## Almost everywhere finitely strongly measurable functions -/
17451752

‎src/measure_theory/group/fundamental_domain.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -212,6 +212,11 @@ calc ∫⁻ x, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂μ : h.linteg
212212
tsum_congr $ λ g, ((measure_preserving_smul g⁻¹ μ).set_lintegral_comp_emb
213213
(measurable_embedding_const_smul _) _ _).symm
214214

215+
216+
@[to_additive] lemma lintegral_eq_tsum'' (h : is_fundamental_domain G s μ) (f : α → ℝ≥0∞) :
217+
∫⁻ x, f x ∂μ = ∑' g : G, ∫⁻ x in s, f (g • x) ∂μ :=
218+
(lintegral_eq_tsum' h f).trans ((equiv.inv G).tsum_eq (λ g, ∫⁻ (x : α) in s, f (g • x) ∂μ))
219+
215220
@[to_additive] lemma set_lintegral_eq_tsum (h : is_fundamental_domain G s μ) (f : α → ℝ≥0∞)
216221
(t : set α) : ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ :=
217222
calc ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂(μ.restrict t) :
@@ -357,6 +362,10 @@ calc ∫ x, f x ∂μ = ∑' g : G, ∫ x in g • s, f x ∂μ : h.integral_eq_
357362
tsum_congr $ λ g, (measure_preserving_smul g⁻¹ μ).set_integral_image_emb
358363
(measurable_embedding_const_smul _) _ _
359364

365+
@[to_additive] lemma integral_eq_tsum'' (h : is_fundamental_domain G s μ)
366+
(f : α → E) (hf : integrable f μ) : ∫ x, f x ∂μ = ∑' g : G, ∫ x in s, f (g • x) ∂μ :=
367+
(integral_eq_tsum' h f hf).trans ((equiv.inv G).tsum_eq (λ g, ∫ (x : α) in s, f (g • x) ∂μ))
368+
360369
@[to_additive] lemma set_integral_eq_tsum (h : is_fundamental_domain G s μ) {f : α → E}
361370
{t : set α} (hf : integrable_on f t μ) :
362371
∫ x in t, f x ∂μ = ∑' g : G, ∫ x in t ∩ g • s, f x ∂μ :=

‎src/measure_theory/measure/haar/quotient.lean‎

Lines changed: 175 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,10 @@ Note that a group `G` with Haar measure that is both left and right invariant is
3333
**unimodular**.
3434
-/
3535

36-
open set measure_theory topological_space measure_theory.measure
37-
open_locale pointwise nnreal
36+
noncomputable theory
37+
38+
open set measure_theory topological_space measure_theory.measure quotient_group
39+
open_locale pointwise measure_theory topology big_operators nnreal ennreal
3840

3941
variables {G : Type*} [group G] [measurable_space G] [topological_space G]
4042
[topological_group G] [borel_space G]
@@ -116,16 +118,15 @@ lemma measure_theory.is_fundamental_domain.is_mul_left_invariant_map [subgroup.n
116118
{ exact hA, },
117119
end }
118120

119-
variables [t2_space (G ⧸ Γ)] [second_countable_topology (G ⧸ Γ)] (K : positive_compacts (G ⧸ Γ))
120-
121121
/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
122122
right-invariant, and a finite volume fundamental domain `𝓕`, the pushforward to the quotient
123123
group `G ⧸ Γ` of the restriction of `μ` to `𝓕` is a multiple of Haar measure on `G ⧸ Γ`. -/
124124
@[to_additive "Given a normal subgroup `Γ` of an additive topological group `G` with Haar measure
125125
`μ`, which is also right-invariant, and a finite volume fundamental domain `𝓕`, the pushforward
126126
to the quotient group `G ⧸ Γ` of the restriction of `μ` to `𝓕` is a multiple of Haar measure on
127127
`G ⧸ Γ`."]
128-
lemma measure_theory.is_fundamental_domain.map_restrict_quotient [subgroup.normal Γ]
128+
lemma measure_theory.is_fundamental_domain.map_restrict_quotient [t2_space (G ⧸ Γ)]
129+
[second_countable_topology (G ⧸ Γ)] (K : positive_compacts (G ⧸ Γ)) [subgroup.normal Γ]
129130
[measure_theory.measure.is_haar_measure μ] [μ.is_mul_right_invariant]
130131
(h𝓕_finite : μ 𝓕 < ⊤) : measure.map (quotient_group.mk' Γ) (μ.restrict 𝓕)
131132
= (μ (𝓕 ∩ (quotient_group.mk' Γ) ⁻¹' K)) • (measure_theory.measure.haar_measure K) :=
@@ -151,12 +152,178 @@ end
151152
topological group `G` with Haar measure `μ`, which is also right-invariant, and a finite volume
152153
fundamental domain `𝓕`, the quotient map to `G ⧸ Γ` is measure-preserving between appropriate
153154
multiples of Haar measure on `G` and `G ⧸ Γ`."]
154-
lemma measure_preserving_quotient_group.mk' [subgroup.normal Γ]
155-
[measure_theory.measure.is_haar_measure μ] [μ.is_mul_right_invariant]
156-
(h𝓕_finite : μ 𝓕 < ⊤) (c : ℝ≥0) (h : μ (𝓕 ∩ (quotient_group.mk' Γ) ⁻¹' K) = c) :
155+
lemma measure_preserving_quotient_group.mk' [t2_space (G ⧸ Γ)] [second_countable_topology (G ⧸ Γ)]
156+
(K : positive_compacts (G ⧸ Γ)) [subgroup.normal Γ] [measure_theory.measure.is_haar_measure μ]
157+
[μ.is_mul_right_invariant] (h𝓕_finite : μ 𝓕 < ⊤) (c : ℝ≥0)
158+
(h : μ (𝓕 ∩ (quotient_group.mk' Γ) ⁻¹' K) = c) :
157159
measure_preserving
158160
(quotient_group.mk' Γ)
159161
(μ.restrict 𝓕)
160162
(c • (measure_theory.measure.haar_measure K)) :=
161163
{ measurable := continuous_quotient_mk.measurable,
162164
map_eq := by rw [h𝓕.map_restrict_quotient K h𝓕_finite, h]; refl }
165+
166+
section
167+
168+
local notation `μ_𝓕` := measure.map (@quotient_group.mk G _ Γ) (μ.restrict 𝓕)
169+
170+
/-- The `ess_sup` of a function `g` on the quotient space `G ⧸ Γ` with respect to the pushforward
171+
of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental domain `𝓕`, is the
172+
same as the `ess_sup` of `g`'s lift to the universal cover `G` with respect to `μ`. -/
173+
@[to_additive "The `ess_sup` of a function `g` on the additive quotient space `G ⧸ Γ` with respect
174+
to the pushforward of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental
175+
domain `𝓕`, is the same as the `ess_sup` of `g`'s lift to the universal cover `G` with respect
176+
to `μ`."]
177+
lemma ess_sup_comp_quotient_group_mk [μ.is_mul_right_invariant] {g : G ⧸ Γ → ℝ≥0∞}
178+
(g_ae_measurable : ae_measurable g μ_𝓕) :
179+
ess_sup g μ_𝓕 = ess_sup (λ (x : G), g x) μ :=
180+
begin
181+
have hπ : measurable (quotient_group.mk : G → G ⧸ Γ) := continuous_quotient_mk.measurable,
182+
rw ess_sup_map_measure g_ae_measurable hπ.ae_measurable,
183+
refine h𝓕.ess_sup_measure_restrict _,
184+
rintros ⟨γ, hγ⟩ x,
185+
dsimp,
186+
congr' 1,
187+
exact quotient_group.mk_mul_of_mem x hγ,
188+
end
189+
190+
/-- Given a quotient space `G ⧸ Γ` where `Γ` is `countable`, and the restriction,
191+
`μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
192+
in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
193+
folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
194+
will take the value `∞` on any open set in the quotient! -/
195+
@[to_additive "Given an additive quotient space `G ⧸ Γ` where `Γ` is `countable`, and the
196+
restriction, `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
197+
in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
198+
folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
199+
will take the value `∞` on any open set in the quotient!"]
200+
lemma _root_.measure_theory.is_fundamental_domain.absolutely_continuous_map
201+
[μ.is_mul_right_invariant] :
202+
map (quotient_group.mk : G → G ⧸ Γ) μ ≪ map (quotient_group.mk : G → G ⧸ Γ) (μ.restrict 𝓕) :=
203+
begin
204+
set π : G → G ⧸ Γ := quotient_group.mk,
205+
have meas_π : measurable π := continuous_quotient_mk.measurable,
206+
apply absolutely_continuous.mk,
207+
intros s s_meas hs,
208+
rw map_apply meas_π s_meas at hs ⊢,
209+
rw measure.restrict_apply at hs,
210+
apply h𝓕.measure_zero_of_invariant _ _ hs,
211+
{ intros γ,
212+
ext g,
213+
rw [set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage],
214+
congrm _ ∈ s,
215+
convert quotient_group.mk_mul_of_mem g (γ⁻¹).2, },
216+
exact measurable_set_preimage meas_π s_meas,
217+
end
218+
219+
local attribute [-instance] quotient.measurable_space
220+
221+
/-- This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of a group `G`, the
222+
integral of a function `f` on `G` with respect to a right-invariant measure `μ` is equal to the
223+
integral over the quotient `G ⧸ Γ` of the automorphization of `f`. -/
224+
@[to_additive "This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of an
225+
additive group `G`, the integral of a function `f` on `G` with respect to a right-invariant
226+
measure `μ` is equal to the integral over the quotient `G ⧸ Γ` of the automorphization of `f`."]
227+
lemma quotient_group.integral_eq_integral_automorphize {E : Type*} [normed_add_comm_group E]
228+
[complete_space E] [normed_space ℝ E] [μ.is_mul_right_invariant] {f : G → E}
229+
(hf₁ : integrable f μ) (hf₂ : ae_strongly_measurable (automorphize f) μ_𝓕) :
230+
∫ x : G, f x ∂μ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :=
231+
calc ∫ x : G, f x ∂μ = ∑' γ : Γ.opposite, ∫ x in 𝓕, f (γ • x) ∂μ : h𝓕.integral_eq_tsum'' f hf₁
232+
... = ∫ x in 𝓕, ∑' γ : Γ.opposite, f (γ • x) ∂μ :
233+
begin
234+
rw integral_tsum,
235+
{ exact λ i, (hf₁.1.comp_quasi_measure_preserving
236+
(measure_preserving_smul i μ).quasi_measure_preserving).restrict, },
237+
{ rw ← h𝓕.lintegral_eq_tsum'' (λ x, ‖f x‖₊),
238+
exact ne_of_lt hf₁.2, },
239+
end
240+
... = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :
241+
(integral_map continuous_quotient_mk.ae_measurable hf₂).symm
242+
243+
/-- This is the **Unfolding Trick**: Given a subgroup `Γ` of a group `G`, the integral of a
244+
function `f` on `G` times the lift to `G` of a function `g` on the quotient `G ⧸ Γ` with respect
245+
to a right-invariant measure `μ` on `G`, is equal to the integral over the quotient of the
246+
automorphization of `f` times `g`. -/
247+
lemma quotient_group.integral_mul_eq_integral_automorphize_mul {K : Type*} [normed_field K]
248+
[complete_space K] [normed_space ℝ K] [μ.is_mul_right_invariant] {f : G → K}
249+
(f_ℒ_1 : integrable f μ) {g : G ⧸ Γ → K} (hg : ae_strongly_measurable g μ_𝓕)
250+
(g_ℒ_infinity : ess_sup (λ x, ↑‖g x‖₊) μ_𝓕 ≠ ∞)
251+
(F_ae_measurable : ae_strongly_measurable (quotient_group.automorphize f) μ_𝓕) :
252+
∫ x : G, g (x : G ⧸ Γ) * (f x) ∂μ = ∫ x : G ⧸ Γ, g x * (quotient_group.automorphize f x) ∂μ_𝓕 :=
253+
begin
254+
let π : G → G ⧸ Γ := quotient_group.mk,
255+
have H₀ : quotient_group.automorphize ((g ∘ π) * f) = g * (quotient_group.automorphize f) :=
256+
quotient_group.automorphize_smul_left f g,
257+
calc ∫ (x : G), g (π x) * f x ∂μ =
258+
∫ (x : G ⧸ Γ), quotient_group.automorphize ((g ∘ π) * f) x ∂μ_𝓕 : _
259+
... = ∫ (x : G ⧸ Γ), g x * (quotient_group.automorphize f x) ∂μ_𝓕 : by simp [H₀],
260+
have meas_π : measurable π := continuous_quotient_mk.measurable,
261+
have H₁ : integrable ((g ∘ π) * f) μ,
262+
{ have : ae_strongly_measurable (λ x : G, g (x : G ⧸ Γ)) μ,
263+
{ refine (ae_strongly_measurable_of_absolutely_continuous _ _ hg).comp_measurable meas_π,
264+
exact h𝓕.absolutely_continuous_map },
265+
refine integrable.ess_sup_smul f_ℒ_1 this _,
266+
{ have hg' : ae_strongly_measurable (λ x, ↑‖g x‖₊) μ_𝓕 :=
267+
(ennreal.continuous_coe.comp continuous_nnnorm).comp_ae_strongly_measurable hg,
268+
rw [← ess_sup_comp_quotient_group_mk h𝓕 hg'.ae_measurable],
269+
exact g_ℒ_infinity } },
270+
have H₂ : ae_strongly_measurable (quotient_group.automorphize ((g ∘ π) * f)) μ_𝓕,
271+
{ simp_rw [H₀],
272+
exact hg.mul F_ae_measurable },
273+
apply quotient_group.integral_eq_integral_automorphize h𝓕 H₁ H₂,
274+
end
275+
276+
end
277+
278+
section
279+
280+
variables {G' : Type*} [add_group G'] [measurable_space G'] [topological_space G']
281+
[topological_add_group G'] [borel_space G']
282+
{μ' : measure G'}
283+
{Γ' : add_subgroup G'}
284+
[countable Γ'] [measurable_space (G' ⧸ Γ')] [borel_space (G' ⧸ Γ')]
285+
{𝓕' : set G'}
286+
287+
local notation `μ_𝓕` := measure.map (@quotient_add_group.mk G' _ Γ') (μ'.restrict 𝓕')
288+
289+
/-- This is the **Unfolding Trick**: Given an additive subgroup `Γ'` of an additive group `G'`, the
290+
integral of a function `f` on `G'` times the lift to `G'` of a function `g` on the quotient
291+
`G' ⧸ Γ'` with respect to a right-invariant measure `μ` on `G'`, is equal to the integral over
292+
the quotient of the automorphization of `f` times `g`. -/
293+
lemma quotient_add_group.integral_mul_eq_integral_automorphize_mul
294+
{K : Type*} [normed_field K]
295+
[complete_space K] [normed_space ℝ K] [μ'.is_add_right_invariant] {f : G' → K}
296+
(f_ℒ_1 : integrable f μ') {g : G' ⧸ Γ' → K} (hg : ae_strongly_measurable g μ_𝓕)
297+
(g_ℒ_infinity : ess_sup (λ x, ↑‖g x‖₊) μ_𝓕 ≠ ∞)
298+
(F_ae_measurable : ae_strongly_measurable (quotient_add_group.automorphize f) μ_𝓕)
299+
(h𝓕 : is_add_fundamental_domain Γ'.opposite 𝓕' μ') :
300+
∫ x : G', g (x : G' ⧸ Γ') * (f x) ∂μ'
301+
= ∫ x : G' ⧸ Γ', g x * (quotient_add_group.automorphize f x) ∂μ_𝓕 :=
302+
begin
303+
let π : G' → G' ⧸ Γ' := quotient_add_group.mk,
304+
have H₀ : quotient_add_group.automorphize ((g ∘ π) * f)
305+
= g * (quotient_add_group.automorphize f) :=
306+
quotient_add_group.automorphize_smul_left f g,
307+
calc ∫ (x : G'), g (π x) * f x ∂μ' =
308+
∫ (x : G' ⧸ Γ'), quotient_add_group.automorphize ((g ∘ π) * f) x ∂μ_𝓕 : _
309+
... = ∫ (x : G' ⧸ Γ'), g x * (quotient_add_group.automorphize f x) ∂μ_𝓕 : by simp [H₀],
310+
have meas_π : measurable π := continuous_quotient_mk.measurable,
311+
have H₁ : integrable ((g ∘ π) * f) μ',
312+
{ have : ae_strongly_measurable (λ x : G', g (x : G' ⧸ Γ')) μ',
313+
{ refine (ae_strongly_measurable_of_absolutely_continuous _ _ hg).comp_measurable meas_π,
314+
exact h𝓕.absolutely_continuous_map },
315+
refine integrable.ess_sup_smul f_ℒ_1 this _,
316+
{ have hg' : ae_strongly_measurable (λ x, ↑‖g x‖₊) μ_𝓕 :=
317+
(ennreal.continuous_coe.comp continuous_nnnorm).comp_ae_strongly_measurable hg,
318+
rw [← ess_sup_comp_quotient_add_group_mk h𝓕 hg'.ae_measurable],
319+
exact g_ℒ_infinity } },
320+
have H₂ : ae_strongly_measurable (quotient_add_group.automorphize ((g ∘ π) * f)) μ_𝓕,
321+
{ simp_rw [H₀],
322+
exact hg.mul F_ae_measurable },
323+
apply quotient_add_group.integral_eq_integral_automorphize h𝓕 H₁ H₂,
324+
end
325+
326+
end
327+
328+
attribute [to_additive quotient_group.integral_mul_eq_integral_automorphize_mul]
329+
quotient_add_group.integral_mul_eq_integral_automorphize_mul

0 commit comments

Comments
 (0)