UpperBound.lean

/-
  Created in 2024 by Gaëtan Serré
-/

/-
  Formalization of the proof on the upper bound of the probability for LIPO to reject a candidate.
-/

import Mathlib.Order.CompletePartialOrder
import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
import LeanLIPO.CompactUtils

open Metric Finset MeasureTheory ENNReal Set

/- The dimension of the space. -/
variable {d : ℕ} (hd : 0 < d)

include hd in
/-- Utility lemma: the the bigger the radius of a ball, the bigger its volume. -/
lemma volume_ball_mono (x₁ x₂ : EuclideanSpace ℝ (Fin d))
    (r₁ r₂ : ℝ) (h : r₁ ≤ r₂) : volume (ball x₁ r₁) ≤ volume (ball x₂ r₂) := byGoals accomplished! 🐙
  d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)have : Nonempty (Fin d) := Fin.pos_iff_nonempty.mp hdd: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)
  d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)repeat d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)rw [d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤ volume (ball x₂ r₂)EuclideanSpace.volume_ball,d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤ volume (ball x₂ r₂)Fintype.card_find: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))]d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))
  d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)have h1 : ENNReal.ofReal (√Real.pi ^ d / ((d : ℝ) / 2 + 1).Gamma) ≠ 0 := d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))byGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))suffices 0 < √Real.pi ^ d / ((d : ℝ) / 2 + 1).Gamma d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≠ 0byGoals accomplished! 🐙
      d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this✝: Nonempty (Fin d)
this: 0 < √Real.pi ^ d / Real.Gamma (↑d / 2 + 1)
ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≠ 0exact (ne_of_lt (ofReal_pos.mpr this)).symmGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))have sqrt_pi_pos : 0 < √Real.pi ^ d := pow_pos (Real.sqrt_pos_of_pos (Real.pi_pos)) dd: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
sqrt_pi_pos: 0 < √Real.pi ^ d
0 < √Real.pi ^ d / Real.Gamma (↑d / 2 + 1)
    d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))have arg_pos : 0 < (d : ℝ) / 2 + 1 := d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
sqrt_pi_pos: 0 < √Real.pi ^ d
0 < √Real.pi ^ d / Real.Gamma (↑d / 2 + 1)byGoals accomplished! 🐙
      d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
sqrt_pi_pos: 0 < √Real.pi ^ d
0 < √Real.pi ^ d / Real.Gamma (↑d / 2 + 1)have : 0 < (d : ℝ) / 2 := half_pos (Nat.cast_pos.mpr hd)d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this✝: Nonempty (Fin d)
sqrt_pi_pos: 0 < √Real.pi ^ d
this: 0 < ↑d / 2
0 < ↑d / 2 + 1
      d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
sqrt_pi_pos: 0 < √Real.pi ^ d
0 < √Real.pi ^ d / Real.Gamma (↑d / 2 + 1)linarithGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))exact div_pos sqrt_pi_pos (Real.Gamma_pos_of_pos arg_pos)Goals accomplished! 🐙
  d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)rw [d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
h1: ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≠ 0
ENNReal.ofReal r₁ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≤
  ENNReal.ofReal r₂ ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))mul_le_mul_right h1 (ofReal_ne_top)d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
h1: ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≠ 0
ENNReal.ofReal r₁ ^ d ≤ ENNReal.ofReal r₂ ^ d]d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
this: Nonempty (Fin d)
h1: ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1)) ≠ 0
ENNReal.ofReal r₁ ^ d ≤ ENNReal.ofReal r₂ ^ d
  d: ℕ
hd: 0 < d
x₁, x₂: EuclideanSpace ℝ (Fin d)
r₁, r₂: ℝ
h: r₁ ≤ r₂
volume (ball x₁ r₁) ≤ volume (ball x₂ r₂)exact pow_le_pow_left' (ofReal_le_ofReal h) dGoals accomplished! 🐙

/--
  `Finset` is a finite set of elements.
  The image of a nonempty `Finset` by a function is also nonempty.
-/
lemma image_nonempty {α β : Type*} [DecidableEq β] {f : α → β} {A : Finset α}
    (ha : A.Nonempty) : (A.image f).Nonempty :=
  (Finset.image_nonempty).mpr ha

/- The search space. -/
variable {X : Set (EuclideanSpace ℝ (Fin d))} (hcompact : IsCompact X) (hne : X.Nonempty)

/- To create the instance `MeasureSpace X` -/
attribute [local instance] Measure.Subtype.measureSpace

/--
  The subtraction operator for the subtype `X`. It uses the operator from the encompassing type.
-/
noncomputable instance : HSub X X (EuclideanSpace ℝ (Fin d)) where
  hSub := fun x y ↦ x.1 - y.1

/-- Definition of the diameter of the image of `X` by a continuous function. -/
noncomputable def diam {f : X → ℝ} (hf : Continuous f) :=
  f (hcompact.exists_argmax hf hne).choose - f (hcompact.exists_argmin hf hne).choose

noncomputable def image_max (f : X → ℝ) {A : Finset X} (hA : A.Nonempty) := (A.image f).max' (image_nonempty hA)

/-- Wether the candidate `x` is being rejected. -/
def is_rejected (f : X → ℝ) {A : Finset X} (hA : A.Nonempty) (κ : ℝ) (x : X) :=
  (A.image (fun y ↦ f y + κ * ‖x - y‖)).min' (image_nonempty hA)
    < image_max f hA
/--
  The set containing all points that are rejected, given a nonempty `Finset`
  of potential maximizers
-/
def rejected (f : X → ℝ) {A : Finset X} (hA : A.Nonempty) (κ : ℝ) :=
  {x | is_rejected f hA κ x}

/--
  A candidate `x` is rejected iff it belongs to a ball determined
  by the best maximizer found so far and a potential maximizer.
-/
theorem reject_iff_ball (f : X → ℝ) {A : Finset X} (hA : A.Nonempty) {κ : ℝ} (hκ : 0 < κ) (x : X) :
    is_rejected f hA κ x
    ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ) := byGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)let f' := image_max f hAd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)show image_max f hA = f' by d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)rflGoals accomplished! 🐙]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)let f'' := (A.image (fun y ↦ f y + κ * ‖x - y‖)).min' (image_nonempty hA)d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)unfold is_rejectedd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
(Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯ < image_max f hA ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
(Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯ < image_max f hA ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)show (A.image (fun y ↦ f y + κ * ‖x - y‖)).min' (image_nonempty hA) = f'' by d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
(Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯ < image_max f hA ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)rflGoals accomplished! 🐙]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
f'' < image_max f hA ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)constructord: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpr(∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)) → f'' < image_max f hA
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)·d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ) d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpr(∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)) → f'' < image_max f hAintro hd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
h: f'' < image_max f hA
mp∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)have : ∃ x₁ ∈ A, f x₁ + κ * ‖x - x₁‖ = f'' := mem_image.mp (min'_mem _ (image_nonempty hA))d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
h: f'' < image_max f hA
this: ∃ x₁ ∈ A, f x₁ + κ * ‖x - x₁‖ = f''
mp∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)rcases this with ⟨x₁, hx₁, hfx₁⟩d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
h: f'' < image_max f hA
x₁: ↑X
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
mp.intro.intro∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)use x₁d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
h: f'' < image_max f hA
x₁: ↑X
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
hx₁ ∈ A ∧ x ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)refine ⟨hx₁, ?_⟩d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
h: f'' < image_max f hA
x₁: ↑X
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
hx ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
h: f'' < image_max f hA
x₁: ↑X
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
hx ∈ ball x₁ ((f' - f x₁) / κ)←hfx₁d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
h: f x₁ + κ * ‖x - x₁‖ < image_max f hA
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
hx ∈ ball x₁ ((f' - f x₁) / κ)]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
h: f x₁ + κ * ‖x - x₁‖ < image_max f hA
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
hx ∈ ball x₁ ((f' - f x₁) / κ) at hd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
h: f x₁ + κ * ‖x - x₁‖ < image_max f hA
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
hx ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)have norm_ineq : ‖x - x₁‖ < (f' - f x₁) / κ :=
      (lt_div_iff₀' hκ).mpr (lt_tsub_iff_left.mpr h)d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
h: f x₁ + κ * ‖x - x₁‖ < image_max f hA
hx₁: x₁ ∈ A
hfx₁: f x₁ + κ * ‖x - x₁‖ = f''
norm_ineq: ‖x - x₁‖ < (f' - f x₁) / κ
hx ∈ ball x₁ ((f' - f x₁) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
mpf'' < image_max f hA → ∃ x₁ ∈ A, x ∈ ball x₁ ((f' - f x₁) / κ)exact norm_ineqGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)rintro ⟨x₁, hx₁, h⟩d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
hx₁: x₁ ∈ A
h: x ∈ ball x₁ ((f' - f x₁) / κ)
mpr.intro.introf'' < image_max f hA
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)have reject : f x₁ + κ * ‖x - x₁‖ < f' :=
    lt_tsub_iff_left.mp ((lt_div_iff₀' hκ).mp (mem_ball_iff_norm.mp h))d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
hx₁: x₁ ∈ A
h: x ∈ ball x₁ ((f' - f x₁) / κ)
reject: f x₁ + κ * ‖x - x₁‖ < f'
mpr.intro.introf'' < image_max f hA
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)have min_le : f'' ≤ f x₁ + κ * ‖x - x₁‖ := min'_le _ _ (mem_image_of_mem _ hx₁)d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
f':= image_max f hA: ℝ
f'':= (Finset.image (fun y => f y + κ * ‖x - y‖) A).min' ⋯: ℝ
x₁: ↑X
hx₁: x₁ ∈ A
h: x ∈ ball x₁ ((f' - f x₁) / κ)
reject: f x₁ + κ * ‖x - x₁‖ < f'
min_le: f'' ≤ f x₁ + κ * ‖x - x₁‖
mpr.intro.introf'' < image_max f hA
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
is_rejected f hA κ x ↔ ∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)exact lt_of_le_of_lt min_le rejectGoals accomplished! 🐙

/-- The set of rejected candidates is equal to the union indexed by `A` of balls.-/
theorem reject_iff_ball_set (f : X → ℝ) {A : Finset X} (hA : A.Nonempty) {κ : ℝ} (hκ : 0 < κ) :
    rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ) := byGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)ext xd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx ∈ rejected f hA κ ↔ x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)constructord: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mpx ∈ rejected f hA κ → x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mprx ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ) → x ∈ rejected f hA κ
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)·d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mpx ∈ rejected f hA κ → x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ) d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mpx ∈ rejected f hA κ → x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mprx ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ) → x ∈ rejected f hA κintro hxd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ rejected f hA κ
h.mpx ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mpx ∈ rejected f hA κ → x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)obtain ⟨x₁, hx₁, hx₁ball⟩ := (reject_iff_ball f hA hκ x).mp hxd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ rejected f hA κ
x₁: ↑X
hx₁: x₁ ∈ A
hx₁ball: x ∈ ball x₁ ((image_max f hA - f x₁) / κ)
h.mp.intro.introx ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
h.mpx ∈ rejected f hA κ → x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)exact Set.mem_biUnion hx₁ hx₁ballGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)intro hxd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
h.mprx ∈ rejected f hA κ
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)suffices is_rejected f hA κ x d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
h.mprx ∈ rejected f hA κbyGoals accomplished! 🐙 d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
this: is_rejected f hA κ x
x ∈ rejected f hA κexact thisGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
h.mpris_rejected f hA κ xreject_iff_ball f hA hκ xd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
h.mpr∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
x: ↑X
hx: x ∈ ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)
h.mpr∃ x₁ ∈ A, x ∈ ball x₁ ((image_max f hA - f x₁) / κ)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
f: ↑X → ℝ
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
rejected f hA κ = ⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)simpa using hxGoals accomplished! 🐙

/-- The diameter is bigger than any distance within `A`. -/
lemma diam_le {f : X → ℝ} (hf : Continuous f) {A : Finset X} (hA : A.Nonempty) :
    ∀ ⦃x⦄, x ∈ A → image_max f hA - f x ≤ diam hcompact hne hf := byGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
∀ ⦃x : ↑X⦄, x ∈ A → image_max f hA - f x ≤ _root_.diam hcompact hne hfintro x _d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
image_max f hA - f x ≤ _root_.diam hcompact hne hf
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
∀ ⦃x : ↑X⦄, x ∈ A → image_max f hA - f x ≤ _root_.diam hcompact hne hfhave image_le_max : image_max f hA ≤ f (hcompact.exists_argmax hf hne).choose := d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
image_max f hA - f x ≤ _root_.diam hcompact hne hfbyGoals accomplished! 🐙
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
image_max f hA - f x ≤ _root_.diam hcompact hne hfhave : ∃ x₁ ∈ A, f x₁ = image_max f hA := mem_image.mp (max'_mem _ (image_nonempty hA))d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
this: ∃ x₁ ∈ A, f x₁ = image_max f hA
image_max f hA ≤ f ⋯.choose
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
image_max f hA - f x ≤ _root_.diam hcompact hne hfrcases this with ⟨x₁, _, hfx₁⟩d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
x₁: ↑X
left✝: x₁ ∈ A
hfx₁: f x₁ = image_max f hA
intro.introimage_max f hA ≤ f ⋯.choose
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
image_max f hA - f x ≤ _root_.diam hcompact hne hfrw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
x₁: ↑X
left✝: x₁ ∈ A
hfx₁: f x₁ = image_max f hA
intro.introimage_max f hA ≤ f ⋯.choose← hfx₁d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
x₁: ↑X
left✝: x₁ ∈ A
hfx₁: f x₁ = image_max f hA
intro.introf x₁ ≤ f ⋯.choose]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
x₁: ↑X
left✝: x₁ ∈ A
hfx₁: f x₁ = image_max f hA
intro.introf x₁ ≤ f ⋯.choose
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
x: ↑X
a✝: x ∈ A
image_max f hA - f x ≤ _root_.diam hcompact hne hfexact (hcompact.exists_argmax hf hne).choose_spec x₁Goals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
∀ ⦃x : ↑X⦄, x ∈ A → image_max f hA - f x ≤ _root_.diam hcompact hne hfexact tsub_le_tsub image_le_max ((hcompact.exists_argmin hf hne).choose_spec x)Goals accomplished! 🐙

/-- The uniform measure on `X`. -/
noncomputable def μ : Measure X := (volume X)⁻¹ • volume

include hcompact in
/--
  Utility lemma. It shows that the volume restricted on `X` of a ball is less or equal
  than the volume on the entire space of the same ball.
-/
lemma le_coe_volume (r : ℝ) (x : X) : volume (ball x r) ≤ volume (ball x.1 r) := byGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)show volume (ball x r) = volume.comap Subtype.val (ball x r) by d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)rflGoals accomplished! 🐙]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
(Measure.comap Subtype.val volume) (ball x r) ≤ volume (ball (↑x) r)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
(Measure.comap Subtype.val volume) (ball x r) ≤ volume (ball (↑x) r)Measure.comap_apply₀ Subtype.val volume Subtype.val_injectived: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hf∀ (s : Set { x // x ∈ X }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hsNullMeasurableSet (ball x r) (Measure.comap Subtype.val volume)]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hf∀ (s : Set { x // x ∈ X }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hsNullMeasurableSet (ball x r) (Measure.comap Subtype.val volume)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)swapd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hf∀ (s : Set { x // x ∈ X }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hsNullMeasurableSet (ball x r) (Measure.comap Subtype.val volume)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)exact fun s a ↦ Measure.MeasurableSet.nullMeasurableSet_subtype_coe hcompact.nullMeasurable ad: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hsNullMeasurableSet (ball x r) (Measure.comap Subtype.val volume)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)swapd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hsNullMeasurableSet (ball x r) (Measure.comap Subtype.val volume)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r);d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
hsNullMeasurableSet (ball x r) (Measure.comap Subtype.val volume)
d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r) d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)exact MeasurableSet.nullMeasurableSet measurableSet_balld: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)suffices Subtype.val '' (ball x r) ⊆ ball x.1 r d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)byGoals accomplished! 🐙
    d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
this: Subtype.val '' ball x r ⊆ ball (↑x) r
volume (Subtype.val '' ball x r) ≤ volume (ball (↑x) r)exact OuterMeasureClass.measure_mono volume thisGoals accomplished! 🐙
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)intro y hyd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
y: EuclideanSpace ℝ (Fin d)
hy: y ∈ Subtype.val '' ball x r
y ∈ ball (↑x) r
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)obtain ⟨x', h1x', h2x'⟩ := (Set.mem_image Subtype.val (ball x r) y).mp hyd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
y: EuclideanSpace ℝ (Fin d)
hy: y ∈ Subtype.val '' ball x r
x': { x // x ∈ X }
h1x': x' ∈ ball x r
h2x': ↑x' = y
intro.introy ∈ ball (↑x) r
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)rw [d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
y: EuclideanSpace ℝ (Fin d)
hy: y ∈ Subtype.val '' ball x r
x': { x // x ∈ X }
h1x': x' ∈ ball x r
h2x': ↑x' = y
intro.introy ∈ ball (↑x) r←h2x'd: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
y: EuclideanSpace ℝ (Fin d)
hy: y ∈ Subtype.val '' ball x r
x': { x // x ∈ X }
h1x': x' ∈ ball x r
h2x': ↑x' = y
intro.intro↑x' ∈ ball (↑x) r]d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
y: EuclideanSpace ℝ (Fin d)
hy: y ∈ Subtype.val '' ball x r
x': { x // x ∈ X }
h1x': x' ∈ ball x r
h2x': ↑x' = y
intro.intro↑x' ∈ ball (↑x) r
  d: ℕ
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
r: ℝ
x: ↑X
volume (ball x r) ≤ volume (ball (↑x) r)exact h1x'Goals accomplished! 🐙

/-- The measure over the entire space of a ball of radius `diam`. -/
noncomputable def measure_ball_diam {f : X → ℝ} (hf : Continuous f) (κ : ℝ) :=
  (volume X)⁻¹
  * (ENNReal.ofReal (diam hcompact hne hf / κ) ^ d
  * ENNReal.ofReal (√Real.pi ^ d / ((d : ℝ) / 2 + 1).Gamma))

include hd hcompact in
/--
  **Main theorem**: the measure of the rejected candidates is less or equal than
  the volume of `|A|` ball of radius `diam`.
-/
theorem measure_reject_le {f : X → ℝ} (hf : Continuous f) {A : Finset X} (hA : A.Nonempty)
    {κ : ℝ} (hκ : 0 < κ) : μ (rejected f hA κ) ≤ A.card * measure_ball_diam hcompact hne hf κ := byGoals accomplished! 🐙
  /- We rewrite the set of rejected candidates as a union of balls. -/
  rw [d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
μ (rejected f hA κ) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κreject_iff_ball_set f hA hκd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κ]d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κ
  /-
    We show that μ ∪(x ∈ A) ball(x, (A.img f).max - f (x))
    ≤ ∑ (x ∈ A) (volume X)⁻¹ * volume (ball((x : ℝᵈ), diam))
  -/
  let diam := diam hcompact hne hfd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κ
  d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
μ (rejected f hA κ) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κhave μ_le : μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ))
      ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball xᵢ.1 (diam / κ)) := d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κbyGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κhave union_le_sum : μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ))
        ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) :=
      measure_biUnion_finset_le A (fun i =>
          ball i (((Finset.image f A).max' (_root_.image_nonempty hA) - f i) / κ))d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
    d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κhave sum_le_sum : ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
      ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball xᵢ.1 (diam / κ)) := d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))byGoals accomplished! 🐙
      d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))have μ_le : ∀ x ∈ A, μ (ball x ((image_max f hA - f x) / κ))
          ≤ (volume X)⁻¹ * volume (ball x.1 (diam / κ)) := d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))byGoals accomplished! 🐙
        d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))intro x hxd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
μ (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))
        d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))have volume_le : volume (ball x ((image_max f hA - f x) / κ))
            ≤ volume (ball x.1 (diam / κ)) := d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
μ (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))byGoals accomplished! 🐙
          d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
μ (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))have volume_comap_le := le_coe_volume
            hcompact ((image_max f hA - f x) / κ) xd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_comap_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) ((image_max f hA - f x) / κ))
volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
          d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
μ (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))have volume_ball_le := volume_ball_mono hd x x _ _
            ((div_le_div_iff_of_pos_right hκ).mpr (diam_le hcompact hne hf hA hx))d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_comap_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) ((image_max f hA - f x) / κ))
volume_ball_le: volume (ball (↑x) ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (_root_.diam hcompact hne hf / κ))
volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
          d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
μ (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))exact Preorder.le_trans _ _ _ volume_comap_le volume_ball_leGoals accomplished! 🐙
        d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))unfold μd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
((volume X)⁻¹ • volume) (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))
        d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))rw [d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
((volume X)⁻¹ • volume) (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))Measure.smul_apply,d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
(volume X)⁻¹ • volume (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ)) d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
((volume X)⁻¹ • volume) (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))smul_eq_muld: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
(volume X)⁻¹ * volume (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))]d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
x: ↑X
hx: x ∈ A
volume_le: volume (ball x ((image_max f hA - f x) / κ)) ≤ volume (ball (↑x) (diam / κ))
(volume X)⁻¹ * volume (ball x ((image_max f hA - f x) / κ)) ≤ (volume X)⁻¹ * volume (ball (↑x) (diam / κ))
        d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))exact mul_le_mul_left' volume_le _Goals accomplished! 🐙
      d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
union_le_sum: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, μ (ball xᵢ ((image_max f hA - f xᵢ) / κ))
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))exact sum_le_sum μ_leGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κexact Preorder.le_trans _ _ _ union_le_sum sum_le_sumGoals accomplished! 🐙
  /-
    We show that ∑ (x ∈ A) (volume X)⁻¹ * volume (ball(x, diam))
    = A.card * (volume X)⁻¹ * volume_ball_diam
  -/
  let measure_ball_diam := measure_ball_diam hcompact hne hf κd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κ
  d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
μ (rejected f hA κ) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κhave sum_μ : ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball xᵢ.1 (diam / κ))
      = A.card * measure_ball_diam := d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κbyGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κhave volume_ball : ∀ x ∈ A, (volume X)⁻¹
      * volume (ball x.1 (diam / κ)) = measure_ball_diam := d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diambyGoals accomplished! 🐙
      d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diamintro x _d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
(volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
      d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diamhave : Nonempty (Fin d) := Fin.pos_iff_nonempty.mp hdd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
this: Nonempty (Fin d)
(volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
      d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diamrw [d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
this: Nonempty (Fin d)
(volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diamEuclideanSpace.volume_ball,d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
this: Nonempty (Fin d)
(volume X)⁻¹ *
    (ENNReal.ofReal (diam / κ) ^ Fintype.card (Fin d) *
      ENNReal.ofReal (√Real.pi ^ Fintype.card (Fin d) / Real.Gamma (↑(Fintype.card (Fin d)) / 2 + 1))) =
  measure_ball_diam d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
this: Nonempty (Fin d)
(volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diamFintype.card_find: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
this: Nonempty (Fin d)
(volume X)⁻¹ * (ENNReal.ofReal (diam / κ) ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))) =
  measure_ball_diam]d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
x: ↑X
a✝: x ∈ A
this: Nonempty (Fin d)
(volume X)⁻¹ * (ENNReal.ofReal (diam / κ) ^ d * ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (↑d / 2 + 1))) =
  measure_ball_diam
      d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diamrflGoals accomplished! 🐙
    d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κrw [d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
volume_ball: ∀ x ∈ A, (volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diamsum_congr rfl volume_ball,d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
volume_ball: ∀ x ∈ A, (volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
∑ x ∈ A, measure_ball_diam = ↑(#A) * measure_ball_diam d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
volume_ball: ∀ x ∈ A, (volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diam← nsmul_eq_muld: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
volume_ball: ∀ x ∈ A, (volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
∑ x ∈ A, measure_ball_diam = #A • measure_ball_diam]d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
volume_ball: ∀ x ∈ A, (volume X)⁻¹ * volume (ball (↑x) (diam / κ)) = measure_ball_diam
∑ x ∈ A, measure_ball_diam = #A • measure_ball_diam
    d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κexact sum_const (measure_ball_diam)Goals accomplished! 🐙
  d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
μ (rejected f hA κ) ≤ ↑(#A) * measure_ball_diam hcompact hne hf κrwa [d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ))
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
sum_μ: ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diam
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κsum_μd: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam
sum_μ: ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diam
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κ]d: ℕ
hd: 0 < d
X: Set (EuclideanSpace ℝ (Fin d))
hcompact: IsCompact X
hne: X.Nonempty
f: ↑X → ℝ
hf: Continuous f
A: Finset ↑X
hA: A.Nonempty
κ: ℝ
hκ: 0 < κ
diam:= _root_.diam hcompact hne hf: ℝ
measure_ball_diam:= _root_.measure_ball_diam hcompact hne hf κ: ℝ≥0∞
μ_le: μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * measure_ball_diam
sum_μ: ∑ xᵢ ∈ A, (volume X)⁻¹ * volume (ball (↑xᵢ) (diam / κ)) = ↑(#A) * measure_ball_diam
μ (⋃ xᵢ ∈ A, ball xᵢ ((image_max f hA - f xᵢ) / κ)) ≤ ↑(#A) * _root_.measure_ball_diam hcompact hne hf κ at μ_leGoals accomplished! 🐙