English
For a fixed positive compact base K0 in a locally compact group G, there is a canonical content on G, called haarContent(K0), which assigns to each compact K the nonnegative quantity ⟨chaar(K0, K), chaar_nonneg(K0, K)⟩ and satisfies monotonicity and additivity on disjoint unions.
Русский
Для локально компактной группы G и фиксированной основы K0 из положительных компактов существует заданное содержимое на G, называемое haarContent(K0), которое сопоставляет каждому компактному K ненегативную величину ⟨chaar(K0, K), chaar_nonneg(K0, K)⟩ и удовлетворяет монотонности и аддитивности на непересекающихся объединениях.
LaTeX
$$$\text{haarContent}_{K_0}(K)=\langle \operatorname{chaar}(K_0,K),\; \operatorname{chaar\_nonneg}(K_0,K)\rangle$$$
Lean4
/-- The function `chaar` interpreted in `ℝ≥0`, as a content -/
@[to_additive /-- additive version of `MeasureTheory.Measure.haar.haarContent` -/
]
noncomputable def haarContent (K₀ : PositiveCompacts G) : Content G
where
toFun K := ⟨chaar K₀ K, chaar_nonneg _ _⟩
mono' K₁ K₂ h := by simp only [← NNReal.coe_le_coe, NNReal.toReal, chaar_mono, h]
sup_disjoint' K₁ K₂ h _h₁ h₂ := by simp only [chaar_sup_eq h]; rfl
sup_le' K₁
K₂ := by
simp only [← NNReal.coe_le_coe, NNReal.coe_add]
simp only [NNReal.toReal, chaar_sup_le]
