case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ ↑↑μ (frontier s) = 0

case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s = ⊤
⊢ ↑↑μ (frontier s) = 0
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
⊢ ↑↑μ (frontier s) = 0
cases' ne_or_eq (affineSpan ℝ s) ⊤ with hspan hspan
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : Set.Nonempty (interior s)
⊢ ↑↑μ (frontier s) = 0
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s = ⊤
⊢ ↑↑μ (frontier s) = 0
rw [← hs.interior_nonempty_iff_affineSpan_eq_top] at hspan
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
⊢ ↑↑μ (frontier s) = 0
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : Set.Nonempty (interior s)
⊢ ↑↑μ (frontier s) = 0
rcases hspan with ⟨x, hx⟩
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
⊢ ↑↑μ (frontier s) = 0

case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
⊢ ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
⊢ ↑↑μ (frontier s) = 0
suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → Bounded t → μ (frontier t) = 0
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Metric.Bounded s
⊢ ↑↑μ (frontier s) = 0
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
⊢ ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
intro s hs hx hb
case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Metric.Bounded s
⊢ ↑↑μ (interior s) ≠ ⊤

case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Metric.Bounded s
⊢ ↑↑μ (frontier s) = 0
replace hb : μ (interior s) ≠ ∞
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Metric.Bounded s
⊢ ↑↑μ (interior s) ≠ ⊤

case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
exact (hb.mono interior_subset).measure_lt_top.ne
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
suffices μ (closure s) ≤ μ (interior s) by
  rwa [frontier, measure_diff interior_subset_closure isOpen_interior.measurableSet hb,
    tsub_eq_zero_iff_le]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
set d : ℕ := FiniteDimensional.finrank ℝ E
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := by
  intro r hr
  refine' (measure_mono <|
    hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq _
  rw [add_haar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
have : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s) :=
  mem_of_superset self_mem_nhdsWithin this
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ Tendsto (fun c => ↑(c ^ d) * ↑↑μ (interior s)) (𝓝[Ioi 1] 1) (𝓝 (↑↑μ (interior s)))
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ↑↑μ (closure s) ≤ ↑↑μ (interior s)
refine' ge_of_tendsto _ this
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ((fun x => x * ↑↑μ (interior s)) ∘ ENNReal.some ∘ fun a => a ^ d) 1 = ↑↑μ (interior s)
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ Tendsto (fun c => ↑(c ^ d) * ↑↑μ (interior s)) (𝓝[Ioi 1] 1) (𝓝 (↑↑μ (interior s)))
refine' (((ENNReal.continuous_mul_const hb).comp
  (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ _).mono_left nhdsWithin_le_nhds
no goals
case H
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
this✝ : ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
this : ∀ᶠ (r : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
⊢ ((fun x => x * ↑↑μ (interior s)) ∘ ENNReal.some ∘ fun a => a ^ d) 1 = ↑↑μ (interior s)
simp
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ frontier s ⊆ ↑(affineSpan ℝ s)
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ ↑↑μ (frontier s) = 0
refine' measure_mono_null _ (add_haar_affineSubspace _ _ hspan)
no goals
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ frontier s ⊆ ↑(affineSpan ℝ s)
exact frontier_subset_closure.trans
  (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
⊢ ↑↑μ (frontier s) = 0
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
⊢ ↑↑μ (frontier s) = 0
let B : ℕ → Set E := fun n => ball x (n + 1)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
this : ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
⊢ ↑↑μ (frontier s) = 0
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
⊢ ↑↑μ (frontier s) = 0
have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 := by
  refine' measure_iUnion_null fun n =>
    H _ (hs.inter (convex_ball _ _)) _ (bounded_ball.mono (inter_subset_right _ _))
  rw [interior_inter, isOpen_ball.interior_eq]
  exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
this : ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
this : ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
⊢ ↑↑μ (frontier s) = 0
refine' measure_mono_null (fun y hy => _) this
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
this : ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
clear this
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
set N : ℕ := ⌊dist y x⌋₊
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ frontier (s ∩ B N)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ ⋃ (n : ℕ), frontier (s ∩ B n)
refine' mem_iUnion.2 ⟨N, _⟩
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N)
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ frontier (s ∩ B N)
have hN : y ∈ B N := by simp [Nat.lt_floor_add_one]
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
this : y ∈ frontier (s ∩ B N) ∩ B N
⊢ y ∈ frontier (s ∩ B N)

case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N)
suffices : y ∈ frontier (s ∩ B N) ∩ B N
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
this : y ∈ frontier (s ∩ B N) ∩ B N
⊢ y ∈ frontier (s ∩ B N)

case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
exact this.1
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (↑N + 1)
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
rw [frontier_inter_open_inter isOpen_ball]
no goals
case this
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (↑N + 1)
exact ⟨hy, hN⟩
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior (s ∩ B n)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
⊢ ↑↑μ (⋃ (n : ℕ), frontier (s ∩ B n)) = 0
refine' measure_iUnion_null fun n =>
  H _ (hs.inter (convex_ball _ _)) _ (bounded_ball.mono (inter_subset_right _ _))
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior s ∩ ball x (↑n + 1)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior (s ∩ B n)
rw [interior_inter, isOpen_ball.interior_eq]
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
n : ℕ
⊢ x ∈ interior s ∩ ball x (↑n + 1)
exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H : ∀ (t : Set E), Convex ℝ t → x ∈ interior t → Metric.Bounded t → ↑↑μ (frontier t) = 0
B : ℕ → Set E := fun n => ball x (↑n + 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ B N
simp [Nat.lt_floor_add_one]
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
this : ↑↑μ (closure s) ≤ ↑↑μ (interior s)
⊢ ↑↑μ (frontier s) = 0
rwa [frontier, measure_diff interior_subset_closure isOpen_interior.measurableSet hb,
  tsub_eq_zero_iff_le]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
⊢ ∀ (r : ℝ≥0), 1 < r → ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
intro r hr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑↑μ (↑(AffineMap.homothety x ↑r) '' interior s) = ↑(r ^ d) * ↑↑μ (interior s)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑↑μ (closure s) ≤ ↑(r ^ d) * ↑↑μ (interior s)
refine' (measure_mono <|
  hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq _
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : MeasureTheory.Measure E
inst✝ : IsAddHaarMeasure μ
s✝ : Set E
hs✝ : Convex ℝ s✝
x : E
hx✝ : x ∈ interior s✝
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : ↑↑μ (interior s) ≠ ⊤
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ ↑↑μ (↑(AffineMap.homothety x ↑r) '' interior s) = ↑(r ^ d) * ↑↑μ (interior s)
rw [add_haar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]