English
Any nontrivial affine subspace of a finite-dimensional real vector space has Haar measure zero.
Русский
Любое не тривиальное аффинное подпространение конечномерного вещественного пространства имеет нулевую гааровскую меру.
LaTeX
$$$\\mu(S) = 0$ for any affine subspace $S$ with $S \\neq E$$$
Lean4
/-- A strict affine subspace has measure zero. -/
theorem addHaar_affineSubspace {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
[FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] (s : AffineSubspace ℝ E) (hs : s ≠ ⊤) : μ s = 0 :=
by
rcases s.eq_bot_or_nonempty with (rfl | hne)
· rw [AffineSubspace.bot_coe, measure_empty]
rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs
rcases hne with ⟨x, hx : x ∈ s⟩
simpa only [AffineSubspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub, sub_eq_add_neg, image_add_right, neg_neg,
measure_preimage_add_right] using addHaar_submodule μ s.direction hs
