English
The scalar factor between two left-invariant measures is non-zero whenever both measures are positive on some open set.
Русский
Масштабный коэффициент между двумя левInvariantными мерами не равен нулю, если обе меры положительны на некотором открытом множестве.
LaTeX
$$$$0 < \\mathrm{haarScalarFactor} (μ' , μ).$$$$
Lean4
/-- In a group with a left invariant measure `μ` and a right invariant measure `ν`, one can express
integrals with respect to `μ` as integrals with respect to `ν` up to a constant scaling factor
(given in the statement as `∫ x, g x ∂μ` where `g` is a fixed reference function) and an
explicit density `y ↦ 1/∫ z, g (z⁻¹ * y) ∂ν`. -/
@[to_additive]
theorem integral_isMulLeftInvariant_isMulRightInvariant_combo {μ ν : Measure G} [IsFiniteMeasureOnCompacts μ]
[IsFiniteMeasureOnCompacts ν] [IsMulLeftInvariant μ] [IsMulRightInvariant ν] [IsOpenPosMeasure ν] {f g : G → ℝ}
(hf : Continuous f) (h'f : HasCompactSupport f) (hg : Continuous g) (h'g : HasCompactSupport g) (g_nonneg : 0 ≤ g)
{x₀ : G} (g_pos : g x₀ ≠ 0) : ∫ x, f x ∂μ = (∫ y, f y * (∫ z, g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ x, g x ∂μ := by
-- The group has to be locally compact, otherwise all integrals vanish and the result is trivial.
rcases h'f.eq_zero_or_locallyCompactSpace_of_group hf with Hf | Hf
· simp [Hf]
let D : G → ℝ := fun (x : G) ↦ ∫ y, g (y⁻¹ * x) ∂ν
have D_cont : Continuous D := continuous_integral_apply_inv_mul hg h'g
have D_pos : ∀ x, 0 < D x := by
intro x
have C : Continuous (fun y ↦ g (y⁻¹ * x)) := hg.comp (continuous_inv.mul continuous_const)
apply (integral_pos_iff_support_of_nonneg _ _).2
· apply C.isOpen_support.measure_pos ν
exact ⟨x * x₀⁻¹, by simpa using g_pos⟩
· exact fun y ↦ g_nonneg (y⁻¹ * x)
· apply C.integrable_of_hasCompactSupport
exact h'g.comp_homeomorph ((Homeomorph.inv G).trans (Homeomorph.mulRight x))
calc
∫ x, f x ∂μ = ∫ x, f x * (D x)⁻¹ * D x ∂μ := by congr with x; rw [mul_assoc, inv_mul_cancel₀ (D_pos x).ne', mul_one]
_ = ∫ x, (∫ y, f x * (D x)⁻¹ * g (y⁻¹ * x) ∂ν) ∂μ := by simp_rw [D, integral_const_mul]
_ = ∫ y, (∫ x, f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ) ∂ν :=
by
apply integral_integral_swap_of_hasCompactSupport
· apply Continuous.mul
· exact (hf.comp continuous_fst).mul ((D_cont.comp continuous_fst).inv₀ (fun x ↦ (D_pos _).ne'))
· exact hg.comp (continuous_snd.inv.mul continuous_fst)
· let K := tsupport f
have K_comp : IsCompact K := h'f
let L := tsupport g
have L_comp : IsCompact L := h'g
let M := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' (K ×ˢ L)
have M_comp : IsCompact M := (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
have M'_comp : IsCompact (closure M) := M_comp.closure
have : ∀ (p : G × G), p ∉ K ×ˢ closure M → f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0 :=
by
rintro ⟨x, y⟩ hxy
by_cases H : x ∈ K; swap
· simp [image_eq_zero_of_notMem_tsupport H]
have : g (y⁻¹ * x) = 0 := by
apply image_eq_zero_of_notMem_tsupport
contrapose! hxy
simp only [mem_prod, H, true_and]
apply subset_closure
simp only [M, mem_image, mem_prod, Prod.exists]
exact ⟨x, y⁻¹ * x, ⟨H, hxy⟩, by group⟩
simp [this]
apply HasCompactSupport.intro' (K_comp.prod M'_comp) ?_ this
exact (isClosed_tsupport f).prod isClosed_closure
_ = ∫ y, (∫ x, f (y * x) * (D (y * x))⁻¹ * g x ∂μ) ∂ν :=
by
congr with y
rw [← integral_mul_left_eq_self _ y]
simp
_ = ∫ x, (∫ y, f (y * x) * (D (y * x))⁻¹ * g x ∂ν) ∂μ :=
by
apply (integral_integral_swap_of_hasCompactSupport _ _).symm
· apply Continuous.mul ?_ (hg.comp continuous_fst)
exact
(hf.comp (continuous_snd.mul continuous_fst)).mul
((D_cont.comp (continuous_snd.mul continuous_fst)).inv₀ (fun x ↦ (D_pos _).ne'))
· let K := tsupport f
have K_comp : IsCompact K := h'f
let L := tsupport g
have L_comp : IsCompact L := h'g
let M := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' (K ×ˢ L)
have M_comp : IsCompact M := (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
have M'_comp : IsCompact (closure M) := M_comp.closure
have : ∀ (p : G × G), p ∉ L ×ˢ closure M → f (p.2 * p.1) * (D (p.2 * p.1))⁻¹ * g p.1 = 0 :=
by
rintro ⟨x, y⟩ hxy
by_cases H : x ∈ L; swap
· simp [image_eq_zero_of_notMem_tsupport H]
have : f (y * x) = 0 := by
apply image_eq_zero_of_notMem_tsupport
contrapose! hxy
simp only [mem_prod, H, true_and]
apply subset_closure
simp only [M, mem_image, mem_prod, Prod.exists]
exact ⟨y * x, x, ⟨hxy, H⟩, by group⟩
simp [this]
apply HasCompactSupport.intro' (L_comp.prod M'_comp) ?_ this
exact (isClosed_tsupport g).prod isClosed_closure
_ = ∫ x, (∫ y, f y * (D y)⁻¹ ∂ν) * g x ∂μ :=
by
simp_rw [integral_mul_const]
congr with x
conv_rhs => rw [← integral_mul_right_eq_self _ x]
_ = (∫ y, f y * (D y)⁻¹ ∂ν) * ∫ x, g x ∂μ := integral_const_mul _ _
