English
Extending innerContent to an outer measure via an induced construction yields equality on opens: μ.outerMeasure U = μ.innerContent U.
Русский
Получение внешней меры из внутреннего содержания по индуцированной схеме дает равенство на открытых множествах: μ.outerMeasure U = μ.innerContent U.
LaTeX
$$$\mu.outerMeasure(U) = \mu.innerContent(U)$ for open U.$$
Lean4
@[to_additive]
theorem innerContent_pos_of_is_mul_left_invariant [Group G] [IsTopologicalGroup G]
(h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G) (hK : μ K ≠ 0)
(U : Opens G) (hU : (U : Set G).Nonempty) : 0 < μ.innerContent U :=
by
have : (interior (U : Set G)).Nonempty := by rwa [U.isOpen.interior_eq]
rcases compact_covered_by_mul_left_translates K.2 this with ⟨s, hs⟩
suffices μ K ≤ s.card * μ.innerContent U by exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2
have : (K : Set G) ⊆ ↑(⨆ g ∈ s, Opens.comap (Homeomorph.mulLeft g : C(G, G)) U) := by
simpa only [Opens.iSup_def, Opens.coe_comap, Subtype.coe_mk]
refine (μ.le_innerContent _ _ this).trans ?_
refine (rel_iSup_sum μ.innerContent μ.innerContent_bot (· ≤ ·) μ.innerContent_iSup_nat _ _).trans ?_
simp only [μ.is_mul_left_invariant_innerContent h3, Finset.sum_const, nsmul_eq_mul, le_refl]
