English
For any left invariant measure μ on a locally compact group, μ is proportional to a Haar measure via haarScalarFactor.
Русский
Для любой левой инвариантной меры μ на локально компактной группе, μ пропорциональна мере Хаара через haarScalarFactor.
LaTeX
$$$$ μ = haarScalarFactor μ' μ \\cdot μ' $$$$
Lean4
/-- Two left invariant measures give the same mass to level sets of continuous compactly supported
functions, up to the scalar `haarScalarFactor μ' μ`.
Auxiliary lemma in the proof of the more general
`measure_isMulInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure. -/
@[to_additive measure_preimage_isAddLeftInvariant_eq_smul_of_hasCompactSupport /--
Two left invariant measures give the same mass to level sets of continuous compactly supported
functions, up to the scalar `addHaarScalarFactor μ' μ`.
Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which works for any set with
compact closure. -/
]
theorem measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport (μ' μ : Measure G) [IsHaarMeasure μ]
[IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {f : G → ℝ} (hf : Continuous f) (h'f : HasCompactSupport f) :
μ' (f ⁻¹' { 1 }) = haarScalarFactor μ' μ • μ (f ⁻¹' { 1 }) := by
/- This follows from the fact that the two measures integrate in the same way continuous
functions, by approximating the indicator function of `f ⁻¹' {1}` by continuous functions
(namely `vₙ ∘ f` where `vₙ` is equal to `1` at `1`, and `0` outside of a small neighborhood
`(1 - uₙ, 1 + uₙ)` where `uₙ` is a sequence tending to `0`).
We use `vₙ = thickenedIndicator uₙ {1}` to take advantage of existing lemmas. -/
obtain ⟨u, -, u_mem, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 1) ∧ Tendsto u atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ) < 1)
let v : ℕ → ℝ → ℝ := fun n x ↦ thickenedIndicator (u_mem n).1 ({ 1 } : Set ℝ) x
have vf_cont n : Continuous ((v n) ∘ f) :=
by
apply Continuous.comp (continuous_induced_dom.comp ?_) hf
exact BoundedContinuousFunction.continuous (thickenedIndicator (u_mem n).left { 1 })
have I :
∀ (ν : Measure G),
IsFiniteMeasureOnCompacts ν →
Tendsto (fun n ↦ ∫ x, v n (f x) ∂ν) atTop (𝓝 (∫ x, Set.indicator ({ 1 } : Set ℝ) (fun _ ↦ 1) (f x) ∂ν)) :=
by
intro ν hν
apply tendsto_integral_of_dominated_convergence (bound := (tsupport f).indicator (fun (_ : G) ↦ (1 : ℝ)))
· exact fun n ↦ (vf_cont n).aestronglyMeasurable
· apply IntegrableOn.integrable_indicator _ (isClosed_tsupport f).measurableSet
simpa using IsCompact.measure_lt_top h'f
· refine fun n ↦ Eventually.of_forall (fun x ↦ ?_)
by_cases hx : x ∈ tsupport f
· simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, indicator_of_mem]
norm_cast
exact thickenedIndicator_le_one _ _ _
· simp only [v, Real.norm_eq_abs, NNReal.abs_eq, hx, not_false_eq_true, indicator_of_notMem]
rw [thickenedIndicator_zero]
· simp
· simpa [image_eq_zero_of_notMem_tsupport hx] using (u_mem n).2.le
· filter_upwards with x
have T :=
tendsto_pi_nhds.1 (thickenedIndicator_tendsto_indicator_closure (fun n ↦ (u_mem n).1) u_lim ({ 1 } : Set ℝ))
(f x)
simp only [thickenedIndicator_apply, closure_singleton] at T
convert NNReal.tendsto_coe.2 T
simp
have M n : ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂(haarScalarFactor μ' μ • μ) :=
by
apply integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ (vf_cont n)
apply h'f.comp_left
simp only [v, thickenedIndicator_apply, NNReal.coe_eq_zero]
rw [thickenedIndicatorAux_zero (u_mem n).1]
· simp only [ENNReal.toNNReal_zero]
· simpa using (u_mem n).2.le
have I1 := I μ' (by infer_instance)
simp_rw [M] at I1
have J1 :
∫ (x : G), indicator { 1 } (fun _ ↦ (1 : ℝ)) (f x) ∂μ' =
∫ (x : G), indicator { 1 } (fun _ ↦ 1) (f x) ∂(haarScalarFactor μ' μ • μ) :=
tendsto_nhds_unique I1 (I (haarScalarFactor μ' μ • μ) (by infer_instance))
have J2 : μ'.real (f ⁻¹' { 1 }) = (haarScalarFactor μ' μ • μ).real (f ⁻¹' { 1 }) :=
by
have : (fun x ↦ indicator { 1 } (fun _ ↦ (1 : ℝ)) (f x)) = (fun x ↦ indicator (f ⁻¹' { 1 }) (fun _ ↦ (1 : ℝ)) x) :=
by
ext x
exact (indicator_comp_right f (s := ({ 1 } : Set ℝ)) (g := (fun _ ↦ (1 : ℝ))) (x := x)).symm
have mf : MeasurableSet (f ⁻¹' { 1 }) := (isClosed_singleton.preimage hf).measurableSet
simpa only [this, mf, integral_indicator_const, smul_eq_mul, mul_one, Pi.smul_apply, nnreal_smul_coe_apply,
ENNReal.toReal_mul, ENNReal.coe_toReal] using J1
have C : IsCompact (f ⁻¹' { 1 }) := h'f.isCompact_preimage hf isClosed_singleton (by simp)
rw [measureReal_eq_measureReal_iff C.measure_lt_top.ne C.measure_lt_top.ne] at J2
simpa using J2
