E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ↑↑μ (closedBall 0 1) = ↑↑μ (ball 0 1)
apply le_antisymm _ (measure_mono ball_subset_closedBall)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A :
  Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1)
    (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)))
⊢ ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
have A : Tendsto
    (fun r : ℝ => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall (0 : E) 1)) (𝓝[<] 1)
      (𝓝 (ENNReal.ofReal ((1 : ℝ) ^ finrank ℝ E) * μ (closedBall (0 : E) 1))) := by
  refine' ENNReal.Tendsto.mul _ (by simp) tendsto_const_nhds (by simp)
  exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
⊢ ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A :
  Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1)
    (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)))
⊢ ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
simp only [one_pow, one_mul, ENNReal.ofReal_one] at A
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
⊢ ∀ᶠ (c : ℝ) in 𝓝[Iio 1] 1, ENNReal.ofReal (c ^ finrank ℝ E) * ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
⊢ ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
refine' le_of_tendsto A _
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
r : ℝ
hr : r ∈ Ioo 0 1
⊢ r ∈ {x | (fun c => ENNReal.ofReal (c ^ finrank ℝ E) * ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)) x}
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
⊢ ∀ᶠ (c : ℝ) in 𝓝[Iio 1] 1, ENNReal.ofReal (c ^ finrank ℝ E) * ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
refine' mem_nhdsWithin_Iio_iff_exists_Ioo_subset.2 ⟨(0 : ℝ), by simp, fun r hr => _⟩
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
r : ℝ
hr : r ∈ Ioo 0 1
⊢ ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
r : ℝ
hr : r ∈ Ioo 0 1
⊢ r ∈ {x | (fun c => ENNReal.ofReal (c ^ finrank ℝ E) * ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)) x}
dsimp
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
r : ℝ
hr : r ∈ Ioo 0 1
⊢ ↑↑μ (closedBall 0 r) ≤ ↑↑μ (ball 0 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
r : ℝ
hr : r ∈ Ioo 0 1
⊢ ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1) ≤ ↑↑μ (ball 0 1)
rw [← add_haar_closedBall' μ (0 : E) hr.1.le]
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
r : ℝ
hr : r ∈ Ioo 0 1
⊢ ↑↑μ (closedBall 0 r) ≤ ↑↑μ (ball 0 1)
exact measure_mono (closedBall_subset_ball hr.2)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[Iio 1] 1) (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E)))
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1)
    (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)))
refine' ENNReal.Tendsto.mul _ (by simp) tendsto_const_nhds (by simp)
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[Iio 1] 1) (𝓝 (ENNReal.ofReal (1 ^ finrank ℝ E)))
exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ENNReal.ofReal (1 ^ finrank ℝ E) ≠ 0 ∨ ↑↑μ (closedBall 0 1) ≠ ⊤
simp
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
⊢ ↑↑μ (closedBall 0 1) ≠ 0 ∨ ENNReal.ofReal (1 ^ finrank ℝ E) ≠ ⊤
simp
no goals
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2005530
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
A : Tendsto (fun r => ENNReal.ofReal (r ^ finrank ℝ E) * ↑↑μ (closedBall 0 1)) (𝓝[Iio 1] 1) (𝓝 (↑↑μ (closedBall 0 1)))
⊢ 0 ∈ Iio 1
simp