English
The chaar is invariant under left translation: chaar(K0, gK) = chaar(K0, K).
Русский
chaar инвариантна относительно левого переноса: chaar(K0, gK) = chaar(K0, K).
LaTeX
$$$\text{chaar}(K_0, (gK)) = \text{chaar}(K_0, K)$$$
Lean4
@[to_additive addCHaar_sup_eq]
theorem chaar_sup_eq {K₀ : PositiveCompacts G} {K₁ K₂ : Compacts G} (h : Disjoint K₁.1 K₂.1) (h₂ : IsClosed K₂.1) :
chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂ :=
by
rcases SeparatedNhds.of_isCompact_isCompact_isClosed K₁.2 K₂.2 h₂ h with ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩
rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩
rcases mem_nhds_iff.mp h1L₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩
replace h2L₁ := Subset.trans (mul_subset_mul_left h1V₁) h2L₁
rcases compact_open_separated_mul_right K₂.2 h1U₂ h2U₂ with ⟨L₂, h1L₂, h2L₂⟩
rcases mem_nhds_iff.mp h1L₂ with ⟨V₂, h1V₂, h2V₂, h3V₂⟩
replace h2L₂ := Subset.trans (mul_subset_mul_left h1V₂) h2L₂
let eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
have : Continuous eval := ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))
rw [eq_comm, ← sub_eq_zero]; change chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)}
let V := V₁ ∩ V₂
apply
mem_of_subset_of_mem _
(chaar_mem_clPrehaar K₀
⟨⟨V⁻¹, (h2V₁.inter h2V₂).preimage continuous_inv⟩, by
simp only [V, mem_inv, inv_one, h3V₁, h3V₂, mem_inter_iff, true_and]⟩)
unfold clPrehaar; rw [IsClosed.closure_subset_iff]
· rintro _ ⟨U, ⟨h1U, h2U, h3U⟩, rfl⟩
simp only [eval, mem_preimage, sub_eq_zero, mem_singleton_iff]; rw [eq_comm]
apply prehaar_sup_eq
· rw [h2U.interior_eq]; exact ⟨1, h3U⟩
· refine disjoint_of_subset ?_ ?_ hU
· refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₁
exact Subset.trans (inv_subset.mpr h1U) inter_subset_left
· refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₂
exact Subset.trans (inv_subset.mpr h1U) inter_subset_right
· apply continuous_iff_isClosed.mp this; exact isClosed_singleton
