case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
⊢ ↑↑μ univ = ⊤
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
⊢ ↑↑μ univ = ⊤
obtain ⟨K, hK, Kclosed, Kint⟩ : ∃ K : Set G, IsCompact K ∧ IsClosed K ∧ (1 : G) ∈ interior K := by
  rcases local_isCompact_isClosed_nhds_of_group (isOpen_univ.mem_nhds (mem_univ (1 : G))) with
    ⟨K, hK⟩
  exact ⟨K, hK.1, hK.2.1, hK.2.2.2⟩
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
⊢ ↑↑μ univ = ⊤
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
⊢ ↑↑μ univ = ⊤
have K_pos : 0 < μ K := measure_pos_of_nonempty_interior _ ⟨_, Kint⟩
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
A : ∀ (L : Set G), IsCompact L → ∃ g, Disjoint L (g • K)
⊢ ↑↑μ univ = ⊤
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
⊢ ↑↑μ univ = ⊤
have A : ∀ L : Set G, IsCompact L → ∃ g : G, Disjoint L (g • K) := fun L hL =>
  exists_disjoint_smul_of_isCompact hL hK
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
⊢ ↑↑μ univ = ⊤
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
A : ∀ (L : Set G), IsCompact L → ∃ g, Disjoint L (g • K)
⊢ ↑↑μ univ = ⊤
choose! g hg using A
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
⊢ ↑↑μ univ = ⊤
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
⊢ ↑↑μ univ = ⊤
set L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
N : Tendsto (fun n => ↑↑μ (L n)) atTop (𝓝 (⊤ * ↑↑μ K))
⊢ ↑↑μ univ = ⊤
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ univ = ⊤
have N : Tendsto (fun n => μ (L n)) atTop (𝓝 (∞ * μ K)) := by
  simp_rw [M]
  apply ENNReal.Tendsto.mul_const _ (Or.inl ENNReal.top_ne_zero)
  exact ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
N : Tendsto (fun n => ↑↑μ (((fun T => T ∪ g T • K)^[n]) K)) atTop (𝓝 ⊤)
⊢ ↑↑μ univ = ⊤
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
N : Tendsto (fun n => ↑↑μ (L n)) atTop (𝓝 (⊤ * ↑↑μ K))
⊢ ↑↑μ univ = ⊤
simp only [ENNReal.top_mul', K_pos.ne', if_false] at N
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
N : Tendsto (fun n => ↑↑μ (((fun T => T ∪ g T • K)^[n]) K)) atTop (𝓝 ⊤)
⊢ ⊤ ≤ ↑↑μ univ
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
N : Tendsto (fun n => ↑↑μ (((fun T => T ∪ g T • K)^[n]) K)) atTop (𝓝 ⊤)
⊢ ↑↑μ univ = ⊤
apply top_le_iff.1
no goals
case intro.intro.intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
N : Tendsto (fun n => ↑↑μ (((fun T => T ∪ g T • K)^[n]) K)) atTop (𝓝 ⊤)
⊢ ⊤ ≤ ↑↑μ univ
exact le_of_tendsto' N fun n => measure_mono (subset_univ _)
case intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K ∧ IsClosed K ∧ K ⊆ univ ∧ 1 ∈ interior K
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ 1 ∈ interior K
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ 1 ∈ interior K
rcases local_isCompact_isClosed_nhds_of_group (isOpen_univ.mem_nhds (mem_univ (1 : G))) with
  ⟨K, hK⟩
no goals
case intro
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K ∧ IsClosed K ∧ K ⊆ univ ∧ 1 ∈ interior K
⊢ ∃ K, IsCompact K ∧ IsClosed K ∧ 1 ∈ interior K
exact ⟨K, hK.1, hK.2.1, hK.2.2.2⟩
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
n : ℕ
⊢ IsCompact (L n)
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
⊢ ∀ (n : ℕ), IsCompact (L n)
intro n
case zero
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
⊢ IsCompact (L Nat.zero)

case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (L (Nat.succ n))
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
n : ℕ
⊢ IsCompact (L n)
induction' n with n IH
no goals
case zero
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
⊢ IsCompact (L Nat.zero)
exact hK
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K)
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (L (Nat.succ n))
simp_rw [iterate_succ']
no goals
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K)
apply IsCompact.union IH (hK.smul (g (L n)))
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
⊢ IsClosed (L n)
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
⊢ ∀ (n : ℕ), IsClosed (L n)
intro n
case zero
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
⊢ IsClosed (L Nat.zero)

case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed (L n)
⊢ IsClosed (L (Nat.succ n))
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
⊢ IsClosed (L n)
induction' n with n IH
no goals
case zero
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
⊢ IsClosed (L Nat.zero)
exact Kclosed
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed (L n)
⊢ IsClosed (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K)
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed (L n)
⊢ IsClosed (L (Nat.succ n))
simp_rw [iterate_succ']
no goals
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed (L n)
⊢ IsClosed (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K)
apply IsClosed.union IH (Kclosed.smul (g (L n)))
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
⊢ ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
⊢ ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
intro n
case zero
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
⊢ ↑↑μ (L Nat.zero) = ↑(Nat.zero + 1) * ↑↑μ K

case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ (L (Nat.succ n)) = ↑(Nat.succ n + 1) * ↑↑μ K
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
⊢ ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
induction' n with n IH
no goals
case zero
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
⊢ ↑↑μ (L Nat.zero) = ↑(Nat.zero + 1) * ↑↑μ K
simp only [one_mul, Nat.cast_one, iterate_zero, id.def, Nat.zero_eq, Nat.zero_add]
no goals
case succ
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ (L (Nat.succ n)) = ↑(Nat.succ n + 1) * ↑↑μ K
calc
  μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
    simp_rw [iterate_succ']
    exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
  _ = (n + 1 + 1 : ℕ) * μ K := by
    simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K) =
    ↑↑μ (((fun T => T ∪ g T • K)^[n]) K) + ↑↑μ (g (((fun T => T ∪ g T • K)^[n]) K) • K)
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ (L (n + 1)) = ↑↑μ (L n) + ↑↑μ (g (L n) • K)
simp_rw [iterate_succ']
no goals
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K) =
    ↑↑μ (((fun T => T ∪ g T • K)^[n]) K) + ↑↑μ (g (((fun T => T ∪ g T • K)^[n]) K) • K)
exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
no goals
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ ↑↑μ (L n) + ↑↑μ (g (L n) • K) = ↑(n + 1 + 1) * ↑↑μ K
simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ Tendsto (fun n => ↑(n + 1) * ↑↑μ K) atTop (𝓝 (⊤ * ↑↑μ K))
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ Tendsto (fun n => ↑↑μ (L n)) atTop (𝓝 (⊤ * ↑↑μ K))
simp_rw [M]
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ Tendsto (fun x => ↑(x + 1)) atTop (𝓝 ⊤)
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ Tendsto (fun n => ↑(n + 1) * ↑↑μ K) atTop (𝓝 (⊤ * ↑↑μ K))
apply ENNReal.Tendsto.mul_const _ (Or.inl ENNReal.top_ne_zero)
no goals
𝕜 : Type ?u.542119
G : Type u_1
H : Type ?u.542125
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : TopologicalSpace G
inst✝⁷ : BorelSpace G
μ✝ : Measure G
inst✝⁶ : Group G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : IsMulLeftInvariant μ✝
inst✝³ : LocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : IsOpenPosMeasure μ
inst✝ : IsMulLeftInvariant μ
K : Set G
hK : IsCompact K
Kclosed : IsClosed K
Kint : 1 ∈ interior K
K_pos : 0 < ↑↑μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => ((fun T => T ∪ g T • K)^[n]) K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), ↑↑μ (L n) = ↑(n + 1) * ↑↑μ K
⊢ Tendsto (fun x => ↑(x + 1)) atTop (𝓝 ⊤)
exact ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)