[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain hα | hα :=
  le_total (card α)
    (bound ε l)
      -- If `card α ≤ bound ε l`, then the partition into singletons is acceptable.
[GOAL]
case inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
refine' ⟨⊥, bot_isEquipartition _, _⟩
[GOAL]
case inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ Finset.card ⊥.parts ∧ Finset.card ⊥.parts ≤ bound ε l ∧ IsUniform ⊥ G ε
[PROOFSTEP]
rw [card_bot, card_univ]
[GOAL]
case inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ IsUniform ⊥ G ε
[PROOFSTEP]
exact
  ⟨hl, hα, botIsUniform _ hε⟩
    -- Else, let's start from a dummy equipartition of size `initialBound ε l`.
[GOAL]
case inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
let t := initialBound ε l
[GOAL]
case inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
have htα : t ≤ (univ : Finset α).card := (initialBound_le_bound _ _).trans (by rwa [Finset.card_univ])
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
⊢ bound ε l ≤ Finset.card univ
[PROOFSTEP]
rwa [Finset.card_univ]
[GOAL]
case inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain ⟨dum, hdum₁, hdum₂⟩ := exists_equipartition_card_eq (univ : Finset α) (initialBound_pos _ _).ne' htα
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain hε₁ | hε₁ := le_total 1 ε
[GOAL]
case inr.intro.intro.inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
exact
  ⟨dum, hdum₁, (le_initialBound ε l).trans hdum₂.ge, hdum₂.le.trans (initialBound_le_bound ε l),
    (dum.isUniformOne G).mono hε₁⟩
    -- Else, set up the induction on energy. We phrase it through the existence for each `i` of an
      -- equipartition of size bounded by `stepBound^[i] (initialBound ε l)` and which is either
      -- `ε`-uniform or has energy at least `ε ^ 5 / 4 * i`.
[GOAL]
case inr.intro.intro.inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
have : Nonempty α := by
  rw [← Fintype.card_pos_iff]
  exact (bound_pos _ _).trans_le hα
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ Nonempty α
[PROOFSTEP]
rw [← Fintype.card_pos_iff]
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ 0 < Fintype.card α
[PROOFSTEP]
exact (bound_pos _ _).trans_le hα
[GOAL]
case inr.intro.intro.inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
suffices h :
  ∀ i,
    ∃ P : Finpartition (univ : Finset α),
      P.IsEquipartition ∧
        t ≤ P.parts.card ∧
          P.parts.card ≤ stepBound^[i] t ∧
            (P.IsUniform G ε ∨ ε ^ 5 / 4 * i ≤ P.energy G)
              -- For `i > 4 / ε ^ 5` we know that the partition we get can't have energy `≥ ε ^ 5 / 4 * i > 1`,
                -- so it must instead be `ε`-uniform and we won.
[GOAL]
case inr.intro.intro.inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := h (⌊4 / ε ^ 5⌋₊ + 1)
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
refine' ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans _, hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) _⟩
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t ≤ bound ε l
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ stepBound (stepBound^[⌊↑4 / ε ^ 5⌋₊] t) ≤ bound ε l
[PROOFSTEP]
exact mul_le_mul_left' (pow_le_pow_of_le_left (by norm_num) (by norm_num) _) _
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 0 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 4 ≤ 16
[PROOFSTEP]
norm_num
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 1 < 1
[PROOFSTEP]
calc
  (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by rw [mul_comm, div_mul_div_cancel 4 (pow_pos hε 5).ne']; norm_num
  _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := ((mul_lt_mul_left <| by positivity).2 (Nat.lt_floor_add_one _))
  _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
  _ ≤ 1 := by exact_mod_cast P.energy_le_one G
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 1 = ε ^ 5 / 4 * (4 / ε ^ 5)
[PROOFSTEP]
rw [mul_comm, div_mul_div_cancel 4 (pow_pos hε 5).ne']
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 1 = 4 / 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 0 < ε ^ 5 / 4
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ ε ^ 5 / ↑4 * (↑⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
[PROOFSTEP]
rwa [← Nat.cast_add_one]
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ ↑(energy P G) ≤ 1
[PROOFSTEP]
exact_mod_cast P.energy_le_one G
[GOAL]
case h
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
[PROOFSTEP]
intro i
[GOAL]
case h
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
[PROOFSTEP]
induction' i with i ih
[GOAL]
case h.zero
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.zero] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑Nat.zero ≤ ↑(energy P G))
[PROOFSTEP]
refine' ⟨dum, hdum₁, hdum₂.ge, hdum₂.le, Or.inr _⟩
[GOAL]
case h.zero
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ε ^ 5 / 4 * ↑Nat.zero ≤ ↑(energy dum G)
[PROOFSTEP]
rw [Nat.cast_zero, mul_zero]
[GOAL]
case h.zero
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ 0 ≤ ↑(energy dum G)
[PROOFSTEP]
exact_mod_cast dum.energy_nonneg G
[GOAL]
case h.succ
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
ih :
  ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := ih
[GOAL]
case h.succ.intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
by_cases huniform : P.IsUniform G ε
[GOAL]
case pos
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : IsUniform P G ε
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
refine' ⟨P, hP₁, hP₂, _, Or.inl huniform⟩
[GOAL]
case pos
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : IsUniform P G ε
⊢ Finset.card P.parts ≤ stepBound^[Nat.succ i] t
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case pos
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : IsUniform P G ε
⊢ Finset.card P.parts ≤ stepBound (stepBound^[i] t)
[PROOFSTEP]
exact
  hP₃.trans
    (le_stepBound _)
      -- Else, `P` must instead have energy at least `ε ^ 5 / 4 * i`.
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : ¬IsUniform P G ε
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
replace hP₄ := hP₄.resolve_left huniform
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hεl' : ↑100 < ↑4 ^ P.parts.card * ε ^ 5 :=
  (hundred_lt_pow_initialBound_mul hε l).trans_le
    (mul_le_mul_of_nonneg_right (pow_le_pow (by norm_num) hP₂) <| by positivity)
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ 1 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ 0 ≤ ε ^ 5
[PROOFSTEP]
positivity
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hi : (i : ℝ) ≤ 4 / ε ^ 5 :=
  by
  have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (by exact_mod_cast P.energy_le_one G)
  rw [div_mul_eq_mul_div, div_le_iff (show (0 : ℝ) < 4 by norm_num)] at hi 
  norm_num at hi 
  rwa [le_div_iff' (pow_pos hε _)]
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (by exact_mod_cast P.energy_le_one G)
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
⊢ ↑(energy P G) ≤ 1
[PROOFSTEP]
exact_mod_cast P.energy_le_one G
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 / 4 * ↑i ≤ 1
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
rw [div_mul_eq_mul_div, div_le_iff (show (0 : ℝ) < 4 by norm_num)] at hi 
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 * ↑i / 4 ≤ 1
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 1 * 4
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
norm_num at hi 
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 4
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
rwa [le_div_iff' (pow_pos hε _)]
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hsize : P.parts.card ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t :=
  hP₃.trans (monotone_iterate_of_id_le le_stepBound (Nat.le_floor hi) _)
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hPα : P.parts.card * 16 ^ P.parts.card ≤ card α :=
  (Nat.mul_le_mul hsize (Nat.pow_le_pow_of_le_right (by norm_num) hsize)).trans hα
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
⊢ 16 > 0
[PROOFSTEP]
norm_num
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
refine'
  ⟨increment hP₁ G ε, increment_isEquipartition hP₁ G ε, _, _,
    Or.inr <| le_trans _ <| energy_increment hP₁ ((seven_le_initialBound ε l).trans hP₂) hεl' hPα huniform hε₁⟩
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ t ≤ Finset.card (increment hP₁ G ε).parts
[PROOFSTEP]
rw [card_increment hPα huniform]
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ t ≤ stepBound (Finset.card P.parts)
[PROOFSTEP]
exact hP₂.trans (le_stepBound _)
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ Finset.card (increment hP₁ G ε).parts ≤ stepBound^[Nat.succ i] t
[PROOFSTEP]
rw [card_increment hPα huniform, iterate_succ_apply']
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ stepBound (Finset.card P.parts) ≤ stepBound (stepBound^[i] t)
[PROOFSTEP]
exact stepBound_mono hP₃
[GOAL]
case neg.refine'_3
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G) + ε ^ 5 / 4
[PROOFSTEP]
rw [Nat.cast_succ, mul_add, mul_one]
[GOAL]
case neg.refine'_3
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑i + ε ^ 5 / 4 ≤ ↑(energy P G) + ε ^ 5 / 4
[PROOFSTEP]
exact add_le_add_right hP₄ _
