English
If s is a proper linear subspace of a finite-dimensional real vector space E equipped with a Haar measure μ, then μ(s) = 0.
Русский
Если s является собственным линейным подпространством конечномерного вещественного пространства E с гааровской мерой μ, то μ(s) = 0.
LaTeX
$$$\\mu(s) = 0$$$
Lean4
/-- A strict vector subspace has measure zero. -/
theorem addHaar_submodule {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
[FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] (s : Submodule ℝ E) (hs : s ≠ ⊤) : μ s = 0 :=
by
obtain ⟨x, hx⟩ : ∃ x, x ∉ s := by simpa only [Submodule.eq_top_iff', not_exists, Ne, not_forall] using hs
obtain ⟨c, cpos, cone⟩ : ∃ c : ℝ, 0 < c ∧ c < 1 := ⟨1 / 2, by simp, by norm_num⟩
have A : IsBounded (range fun n : ℕ => c ^ n • x) :=
have : Tendsto (fun n : ℕ => c ^ n • x) atTop (𝓝 ((0 : ℝ) • x)) :=
(tendsto_pow_atTop_nhds_zero_of_lt_one cpos.le cone).smul_const x
isBounded_range_of_tendsto _ this
apply addHaar_eq_zero_of_disjoint_translates μ _ A _ (Submodule.closed_of_finiteDimensional s).measurableSet
intro m n hmn
simp only [Function.onFun, image_add_left, singleton_add, disjoint_left, mem_preimage, SetLike.mem_coe]
intro y hym hyn
have A : (c ^ n - c ^ m) • x ∈ s := by
convert s.sub_mem hym hyn using 1
simp only [sub_smul, neg_sub_neg, add_sub_add_right_eq_sub]
have H : c ^ n - c ^ m ≠ 0 := by
simpa only [sub_eq_zero, Ne] using (pow_right_strictAnti₀ cpos cone).injective.ne hmn.symm
have : x ∈ s := by
convert s.smul_mem (c ^ n - c ^ m)⁻¹ A
rw [smul_smul, inv_mul_cancel₀ H, one_smul]
exact hx this
