[GOAL]
n : ℕ
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
a b : ℕ
h : a ≤ b
⊢ 4 > 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ 0 < 4 ^ n
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ ε : ℝ
n : ℕ
h : ↑100 ≤ 4 ^ n * ε ^ 5
⊢ Odd 5
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ ε : ℝ
n : ℕ
h : ↑100 ≤ 4 ^ n * ε ^ 5
⊢ 0 < 100
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ ε : ℝ
n : ℕ
h : ↑100 ≤ 4 ^ n * ε ^ 5
⊢ 0 ≤ 4 ^ n
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ 4 ≤ 16
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ 0 < Fintype.card α / stepBound (Finset.card P.parts)
[PROOFSTEP]
sz_positivity
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
⊢ 0 < ↑(Fintype.card α / stepBound (Finset.card P.parts)) + 1
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
⊢ 0 < 100
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
⊢ 0 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
⊢ Odd 5
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
⊢ 0 ≤ 4 ^ Finset.card P.parts
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
⊢ 4 ^ Finset.card P.parts ≤ ↑(Fintype.card α / stepBound (Finset.card P.parts))
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
⊢ 4 ^ Finset.card P.parts ≤ Fintype.card α / stepBound (Finset.card P.parts)
[PROOFSTEP]
rwa [Nat.le_div_iff_mul_le' (stepBound_pos (P.parts_nonempty <| univ_nonempty.ne_empty).card_pos), stepBound,
  mul_left_comm, ← mul_pow]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 100 ≤ Fintype.card α / stepBound (Finset.card P.parts)
[PROOFSTEP]
exact_mod_cast
  (hundred_div_ε_pow_five_le_m hPα hPε).trans'
    (le_div_self (by norm_num) (by sz_positivity) <| pow_le_one _ (by sz_positivity) hε)
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 0 ≤ ↑100
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 0 < ε ^ 5
[PROOFSTEP]
sz_positivity
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
inst✝ : Nonempty α
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
hPε : ↑100 ≤ 4 ^ Finset.card P.parts * ε ^ 5
hε : ε ≤ 1
⊢ 0 ≤ ε
[PROOFSTEP]
sz_positivity
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
⊢ Fintype.card α / Finset.card P.parts - Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
      1 ≤
    4 ^ Finset.card P.parts
[PROOFSTEP]
have h : 1 ≤ 4 ^ P.parts.card := one_le_pow_of_one_le (by norm_num) _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
⊢ 1 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
⊢ Fintype.card α / Finset.card P.parts - Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
      1 ≤
    4 ^ Finset.card P.parts
[PROOFSTEP]
rw [stepBound, ← Nat.div_div_eq_div_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
⊢ Fintype.card α / Finset.card P.parts -
        Fintype.card α / Finset.card P.parts / 4 ^ Finset.card P.parts * 4 ^ Finset.card P.parts +
      1 ≤
    4 ^ Finset.card P.parts
[PROOFSTEP]
conv_rhs => rw [← Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
| 4 ^ Finset.card P.parts
[PROOFSTEP]
rw [← Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
| 4 ^ Finset.card P.parts
[PROOFSTEP]
rw [← Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
| 4 ^ Finset.card P.parts
[PROOFSTEP]
rw [← Nat.sub_add_cancel h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
⊢ Fintype.card α / Finset.card P.parts -
        Fintype.card α / Finset.card P.parts / 4 ^ Finset.card P.parts * 4 ^ Finset.card P.parts +
      1 ≤
    4 ^ Finset.card P.parts - 1 + 1
[PROOFSTEP]
rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
h : 1 ≤ 4 ^ Finset.card P.parts
⊢ Fintype.card α / Finset.card P.parts ≤
    Fintype.card α / Finset.card P.parts / 4 ^ Finset.card P.parts * 4 ^ Finset.card P.parts + 4 ^ Finset.card P.parts -
      1
[PROOFSTEP]
exact Nat.le_pred_of_lt (Nat.lt_div_mul_add h)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hucard :
  Finset.card u =
    Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
      (Fintype.card α / Finset.card P.parts -
        Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)
⊢ (4 ^ Finset.card P.parts -
          (Fintype.card α / Finset.card P.parts -
            Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)) *
        (Fintype.card α / stepBound (Finset.card P.parts)) +
      (Fintype.card α / Finset.card P.parts -
          Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts) *
        (Fintype.card α / stepBound (Finset.card P.parts) + 1) =
    Finset.card u
[PROOFSTEP]
rw [hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
  Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), mul_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
hucard :
  ¬Finset.card u =
      Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
        (Fintype.card α / Finset.card P.parts -
          Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)
⊢ (4 ^ Finset.card P.parts -
          (Fintype.card α / Finset.card P.parts -
              Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
            1)) *
        (Fintype.card α / stepBound (Finset.card P.parts)) +
      (Fintype.card α / Finset.card P.parts -
            Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
          1) *
        (Fintype.card α / stepBound (Finset.card P.parts) + 1) =
    Finset.card u
[PROOFSTEP]
have : m * 4 ^ P.parts.card ≤ card α / P.parts.card :=
  by
  rw [stepBound, ← Nat.div_div_eq_div_mul]
  exact Nat.div_mul_le_self _ _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
hucard :
  ¬Finset.card u =
      Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
        (Fintype.card α / Finset.card P.parts -
          Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)
⊢ Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts ≤ Fintype.card α / Finset.card P.parts
[PROOFSTEP]
rw [stepBound, ← Nat.div_div_eq_div_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
hucard :
  ¬Finset.card u =
      Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
        (Fintype.card α / Finset.card P.parts -
          Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)
⊢ Fintype.card α / Finset.card P.parts / 4 ^ Finset.card P.parts * 4 ^ Finset.card P.parts ≤
    Fintype.card α / Finset.card P.parts
[PROOFSTEP]
exact Nat.div_mul_le_self _ _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
hucard :
  ¬Finset.card u =
      Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
        (Fintype.card α / Finset.card P.parts -
          Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts)
this : Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts ≤ Fintype.card α / Finset.card P.parts
⊢ (4 ^ Finset.card P.parts -
          (Fintype.card α / Finset.card P.parts -
              Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
            1)) *
        (Fintype.card α / stepBound (Finset.card P.parts)) +
      (Fintype.card α / Finset.card P.parts -
            Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
          1) *
        (Fintype.card α / stepBound (Finset.card P.parts) + 1) =
    Finset.card u
[PROOFSTEP]
rw [Nat.add_sub_of_le this] at hucard
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
hucard : ¬Finset.card u = Fintype.card α / Finset.card P.parts
this : Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts ≤ Fintype.card α / Finset.card P.parts
⊢ (4 ^ Finset.card P.parts -
          (Fintype.card α / Finset.card P.parts -
              Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
            1)) *
        (Fintype.card α / stepBound (Finset.card P.parts)) +
      (Fintype.card α / Finset.card P.parts -
            Fintype.card α / stepBound (Finset.card P.parts) * 4 ^ Finset.card P.parts +
          1) *
        (Fintype.card α / stepBound (Finset.card P.parts) + 1) =
    Finset.card u
[PROOFSTEP]
rw [(hP.card_parts_eq_average hu).resolve_left hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
  Nat.sub_add_cancel a_add_one_le_four_pow_parts_card, ← add_assoc, mul_comm, Nat.add_sub_of_le this, card_univ]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
⊢ 4 ^ Finset.card P.parts * ↑(Fintype.card α / stepBound (Finset.card P.parts)) ≤ ↑(Finset.card u)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
⊢ 4 ^ Finset.card P.parts * (Fintype.card α / stepBound (Finset.card P.parts)) ≤ Finset.card u
[PROOFSTEP]
rw [stepBound, ← Nat.div_div_eq_div_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
hP : Finpartition.IsEquipartition P
hu : u ∈ P.parts
⊢ 4 ^ Finset.card P.parts * (Fintype.card α / Finset.card P.parts / 4 ^ Finset.card P.parts) ≤ Finset.card u
[PROOFSTEP]
exact (Nat.mul_div_le _ _).trans (hP.average_le_card_part hu)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ ↑100 < 4 ^ initialBound ε l * ε ^ 5
[PROOFSTEP]
rw [← rpow_nat_cast 4, ← div_lt_iff (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ← div_lt_iff, initialBound,
  Nat.cast_max, Nat.cast_max]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (↑100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (↑100 / ε ^ 5) / log 4⌋₊ + 1))
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max 7 (max (↑l) (↑⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))
[PROOFSTEP]
exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < log 4
[PROOFSTEP]
exact log_pos (by norm_num)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 1 < 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < ↑100 / ε ^ 5
[PROOFSTEP]
exact div_pos (by norm_num) (pow_pos hε 5)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ : ℝ
l✝ : ℕ
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 0 < ↑100
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
⊢ 0 < 16 ^ stepBound^[⌊↑4 / ε ^ 5⌋₊] (initialBound ε l)
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
⊢ d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
obtain hscard | hscard := (s.card.cast_nonneg : (0 : 𝕜) ≤ s.card).eq_or_lt
[GOAL]
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 = ↑(Finset.card s)
⊢ d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
simpa [← hscard] using ht.trans sum_div_card_sq_le_sum_sq_div_card
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
⊢ d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
have htcard : (0 : 𝕜) < t.card := hscard.trans_le (Nat.cast_le.2 (card_le_of_subset hst))
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
⊢ d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
have h₁ : x ^ 2 ≤ ((∑ i in s, f i) / s.card - (∑ i in t, f i) / t.card) ^ 2 := sq_le_sq.2 (by rwa [abs_of_nonneg hx])
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
⊢ |x| ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
[PROOFSTEP]
rwa [abs_of_nonneg hx]
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
⊢ d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
have h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / t.card)) / s.card) ^ 2 :=
  by
  apply h₁.trans
  rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left _ hscard.ne']
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
⊢ x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
[PROOFSTEP]
apply h₁.trans
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
⊢ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2 ≤
    ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
[PROOFSTEP]
rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left _ hscard.ne']
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
⊢ d + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤ (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
apply (add_le_add_right ht _).trans
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
⊢ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 + ↑(Finset.card s) / ↑(Finset.card t) * x ^ 2 ≤
    (∑ i in t, f i ^ 2) / ↑(Finset.card t)
[PROOFSTEP]
rw [← mul_div_right_comm, le_div_iff htcard, add_mul, div_mul_cancel _ htcard.ne']
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
⊢ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) + ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, f i ^ 2
[PROOFSTEP]
have h₃ := mul_sq_le_sum_sq hst (fun i => (f i - (∑ j in t, f j) / t.card)) h₂ hscard.ne'
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) + ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, f i ^ 2
[PROOFSTEP]
apply (add_le_add_left h₃ _).trans
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) +
      ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2 ≤
    ∑ i in t, f i ^ 2
[PROOFSTEP]
simp_rw [sub_div' _ _ _ htcard.ne']
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) +
      ∑ x in t, ((f x * ↑(Finset.card t) - ∑ i in t, f i) / ↑(Finset.card t)) ^ 2 ≤
    ∑ i in t, f i ^ 2
[PROOFSTEP]
conv_lhs => enter [2, 2, x]; rw [div_pow]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
| ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) +
    ∑ x in t, ((f x * ↑(Finset.card t) - ∑ i in t, f i) / ↑(Finset.card t)) ^ 2
[PROOFSTEP]
enter [2, 2, x]; rw [div_pow]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
| ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) +
    ∑ x in t, ((f x * ↑(Finset.card t) - ∑ i in t, f i) / ↑(Finset.card t)) ^ 2
[PROOFSTEP]
enter [2, 2, x]; rw [div_pow]
[GOAL]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
| ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) +
    ∑ x in t, ((f x * ↑(Finset.card t) - ∑ i in t, f i) / ↑(Finset.card t)) ^ 2
[PROOFSTEP]
enter [2, 2, x]
[GOAL]
case h
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x✝ : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x✝
hs : x✝ ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x✝ ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x✝ ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x✝ ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
x : ι
| ((f x * ↑(Finset.card t) - ∑ i in t, f i) / ↑(Finset.card t)) ^ 2
[PROOFSTEP]
rw [div_pow]
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2 * ↑(Finset.card t) +
      ∑ x in t, (f x * ↑(Finset.card t) - ∑ i in t, f i) ^ 2 / ↑(Finset.card t) ^ 2 ≤
    ∑ i in t, f i ^ 2
[PROOFSTEP]
rw [div_pow, ← sum_div, ← mul_div_right_comm _ (t.card : 𝕜), ← add_div, div_le_iff (sq_pos_of_ne_zero _ htcard.ne')]
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ (∑ i in t, f i) ^ 2 * ↑(Finset.card t) + ∑ x in t, (f x * ↑(Finset.card t) - ∑ i in t, f i) ^ 2 ≤
    (∑ i in t, f i ^ 2) * ↑(Finset.card t) ^ 2
[PROOFSTEP]
simp_rw [sub_sq, sum_add_distrib, sum_const, nsmul_eq_mul, sum_sub_distrib, mul_pow, ← sum_mul, ← mul_sum, ← sum_mul]
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ (∑ i in t, f i) ^ 2 * ↑(Finset.card t) +
      ((∑ x in t, f x ^ 2) * ↑(Finset.card t) ^ 2 - 2 * ((∑ i in t, f i) * ↑(Finset.card t)) * ∑ i in t, f i +
        ↑(Finset.card t) * (∑ i in t, f i) ^ 2) ≤
    (∑ i in t, f i ^ 2) * ↑(Finset.card t) ^ 2
[PROOFSTEP]
ring_nf
[GOAL]
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
P : Finpartition univ
u : Finset α
ε : ℝ
l : ℕ
ι : Type u_2
𝕜 : Type u_3
inst✝¹ : LinearOrderedField 𝕜
r : ι → ι → Prop
inst✝ : DecidableRel r
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)|
ht : d ≤ ((∑ i in t, f i) / ↑(Finset.card t)) ^ 2
hscard : 0 < ↑(Finset.card s)
htcard : 0 < ↑(Finset.card t)
h₁ : x ^ 2 ≤ ((∑ i in s, f i) / ↑(Finset.card s) - (∑ i in t, f i) / ↑(Finset.card t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i in s, (f i - (∑ j in t, f j) / ↑(Finset.card t))) / ↑(Finset.card s)) ^ 2
h₃ : ↑(Finset.card s) * x ^ 2 ≤ ∑ i in t, (fun i => f i - (∑ j in t, f j) / ↑(Finset.card t)) i ^ 2
⊢ ↑(Finset.card t) ^ 2 * ∑ x in t, f x ^ 2 ≤ ↑(Finset.card t) ^ 2 * ∑ x in t, f x ^ 2
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ ε : ℝ
l : ℕ
⊢ 0 < initialBound ε l
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
ε✝ ε : ℝ
l : ℕ
⊢ 0 < bound ε l
[PROOFSTEP]
positivity