E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
borelize E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
let μ : Measure E := Measure.addHaar
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
let δ : ℝ := (1 : ℝ) / 2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
let ρ : ℝ := (5 : ℝ) / 2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
have ρpos : 0 < ρ := by norm_num [ρ]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
set A := ⋃ c ∈ s, ball (c : E) δ with hA
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
have D : Set.Pairwise (s : Set E) (Disjoint on fun c => ball (c : E) δ) := by
  rintro c hc d hd hcd
  apply ball_disjoint_ball
  rw [dist_eq_norm]
  convert h c hc d hd hcd
  norm_num
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
have A_subset : A ⊆ ball (0 : E) ρ := by
  refine' iUnion₂_subset fun x hx => _
  apply ball_subset_ball'
  calc
    δ + dist x 0 ≤ δ + 2 := by rw [dist_zero_right]; exact add_le_add le_rfl (hs x hx)
    _ = 5 / 2 := by norm_num [δ]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
have I :
  (s.card : ℝ≥0∞) * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1) :=
  calc
    (s.card : ℝ≥0∞) * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) = μ A := by
      rw [hA, measure_biUnion_finset D fun c _ => measurableSet_ball]
      have I : 0 < δ := by norm_num [δ]
      simp only [div_pow, μ.add_haar_ball_of_pos _ I]
      simp only [one_div, one_pow, Finset.sum_const, nsmul_eq_mul, mul_assoc]
    _ ≤ μ (ball (0 : E) ρ) := (measure_mono A_subset)
    _ = ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1) := by
      simp only [μ.add_haar_ball_of_pos _ ρpos]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
have J : (s.card : ℝ≥0∞) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) :=
  (ENNReal.mul_le_mul_right (measure_ball_pos _ _ zero_lt_one).ne' measure_ball_lt_top.ne).1 I
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
K : ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
have K : (s.card : ℝ) ≤ (5 : ℝ) ^ finrank ℝ E := by
  have := ENNReal.toReal_le_of_le_ofReal (pow_nonneg ρpos.le _) J
  simp [ENNReal.toReal_mul] at this
  simpa [div_eq_mul_inv, zero_le_two] using this
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
K : ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
⊢ Finset.card s ≤ 5 ^ finrank ℝ E
exact_mod_cast K
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
⊢ 0 < ρ
norm_num [ρ]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ (Disjoint on fun c => ball c δ) c d
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
⊢ Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
rintro c hc d hd hcd
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ δ + δ ≤ dist c d
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ (Disjoint on fun c => ball c δ) c d
apply ball_disjoint_ball
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ δ + δ ≤ ‖c - d‖
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ δ + δ ≤ dist c d
rw [dist_eq_norm]
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ δ + δ = 1
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ δ + δ ≤ ‖c - d‖
convert h c hc d hd hcd
no goals
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
c : E
hc : c ∈ ↑s
d : E
hd : d ∈ ↑s
hcd : c ≠ d
⊢ δ + δ = 1
norm_num
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ ball x δ ⊆ ball 0 ρ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
⊢ A ⊆ ball 0 ρ
refine' iUnion₂_subset fun x hx => _
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ δ + dist x 0 ≤ ρ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ ball x δ ⊆ ball 0 ρ
apply ball_subset_ball'
no goals
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ δ + dist x 0 ≤ ρ
calc
  δ + dist x 0 ≤ δ + 2 := by rw [dist_zero_right]; exact add_le_add le_rfl (hs x hx)
  _ = 5 / 2 := by norm_num [δ]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ δ + ‖x‖ ≤ δ + 2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ δ + dist x 0 ≤ δ + 2
rw [dist_zero_right]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ δ + ‖x‖ ≤ δ + 2
exact add_le_add le_rfl (hs x hx)
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
x : E
hx : x ∈ s
⊢ δ + 2 = 5 / 2
norm_num [δ]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) = Finset.sum s fun p => ↑↑μ (ball p δ)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) = ↑↑μ A
rw [hA, measure_biUnion_finset D fun c _ => measurableSet_ball]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I : 0 < δ
⊢ ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) = Finset.sum s fun p => ↑↑μ (ball p δ)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) = Finset.sum s fun p => ↑↑μ (ball p δ)
have I : 0 < δ := by norm_num [δ]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I : 0 < δ
⊢ ↑(Finset.card s) * ENNReal.ofReal (1 ^ finrank ℝ E / 2 ^ finrank ℝ E) * ↑↑Measure.addHaar (ball 0 1) =
    Finset.sum s fun x => ENNReal.ofReal (1 ^ finrank ℝ E / 2 ^ finrank ℝ E) * ↑↑Measure.addHaar (ball 0 1)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I : 0 < δ
⊢ ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) = Finset.sum s fun p => ↑↑μ (ball p δ)
simp only [div_pow, μ.add_haar_ball_of_pos _ I]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I : 0 < δ
⊢ ↑(Finset.card s) * ENNReal.ofReal (1 ^ finrank ℝ E / 2 ^ finrank ℝ E) * ↑↑Measure.addHaar (ball 0 1) =
    Finset.sum s fun x => ENNReal.ofReal (1 ^ finrank ℝ E / 2 ^ finrank ℝ E) * ↑↑Measure.addHaar (ball 0 1)
simp only [one_div, one_pow, Finset.sum_const, nsmul_eq_mul, mul_assoc]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ 0 < δ
norm_num [δ]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
⊢ ↑↑μ (ball 0 ρ) = ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
simp only [μ.add_haar_ball_of_pos _ ρpos]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
this : ENNReal.toReal (↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E)) ≤ ρ ^ finrank ℝ E
⊢ ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
⊢ ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
have := ENNReal.toReal_le_of_le_ofReal (pow_nonneg ρpos.le _) J
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
this : ↑(Finset.card s) * ENNReal.toReal (ENNReal.ofReal (2 ^ finrank ℝ E)⁻¹) ≤ 5 ^ finrank ℝ E / 2 ^ finrank ℝ E
⊢ ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
this : ENNReal.toReal (↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E)) ≤ ρ ^ finrank ℝ E
⊢ ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
simp [ENNReal.toReal_mul] at this
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ (c : E), c ∈ s → ‖c‖ ≤ 2
h : ∀ (c : E), c ∈ s → ∀ (d : E), d ∈ s → c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : MeasureTheory.Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ (c : E) (_ : c ∈ s), ball c δ
hA : A = ⋃ (c : E) (_ : c ∈ s), ball c δ
D : Set.Pairwise (↑s) (Disjoint on fun c => ball c δ)
A_subset : A ⊆ ball 0 ρ
I :
  ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) * ↑↑μ (ball 0 1) ≤
    ENNReal.ofReal (ρ ^ finrank ℝ E) * ↑↑μ (ball 0 1)
J : ↑(Finset.card s) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
this : ↑(Finset.card s) * ENNReal.toReal (ENNReal.ofReal (2 ^ finrank ℝ E)⁻¹) ≤ 5 ^ finrank ℝ E / 2 ^ finrank ℝ E
⊢ ↑(Finset.card s) ≤ 5 ^ finrank ℝ E
simpa [div_eq_mul_inv, zero_le_two] using this