[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ x ∈ box n d ↔ ∀ (i : Fin n), x i < d
[PROOFSTEP]
simp only [box, Fintype.mem_piFinset, mem_range]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ card (box n d) = d ^ n
[PROOFSTEP]
simp [box]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ box (n + 1) 0 = ∅
[PROOFSTEP]
simp [box]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ x : Fin n → ℕ
⊢ x ∈ sphere n d 0 → x ∈ 0
[PROOFSTEP]
simp [sphere, Function.funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k✝ N : ℕ
x : Fin n✝ → ℕ
n k : ℕ
⊢ sphere (n + 1) 0 k = ∅
[PROOFSTEP]
simp [sphere]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ ‖↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x)‖ = Real.sqrt ↑k
[PROOFSTEP]
rw [EuclideanSpace.norm_eq]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Real.sqrt (∑ i : Fin n, ‖↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x) i‖ ^ 2) = Real.sqrt ↑k
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Real.sqrt (∑ i : Fin n, |↑(x i)| ^ 2) = Real.sqrt ↑k
[PROOFSTEP]
simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ ↑(sphere n d k)
⊢ x ∈ (fun x => ↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 (Real.sqrt ↑k)
[PROOFSTEP]
rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]
[GOAL]
α : Type u_1
β : Type u_2
n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
⊢ (fun a => ∑ i : Fin n, a i * d ^ ↑i) 0 = 0
[PROOFSTEP]
simp_rw [Pi.zero_apply, zero_mul, sum_const_zero]
[GOAL]
α : Type u_1
β : Type u_2
n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
a b : Fin n → ℕ
⊢ ZeroHom.toFun
      { toFun := fun a => ∑ i : Fin n, a i * d ^ ↑i, map_zero' := (_ : (fun a => ∑ i : Fin n, a i * d ^ ↑i) 0 = 0) }
      (a + b) =
    ZeroHom.toFun
        { toFun := fun a => ∑ i : Fin n, a i * d ^ ↑i, map_zero' := (_ : (fun a => ∑ i : Fin n, a i * d ^ ↑i) 0 = 0) }
        a +
      ZeroHom.toFun
        { toFun := fun a => ∑ i : Fin n, a i * d ^ ↑i, map_zero' := (_ : (fun a => ∑ i : Fin n, a i * d ^ ↑i) 0 = 0) } b
[PROOFSTEP]
simp_rw [Pi.add_apply, add_mul, sum_add_distrib]
[GOAL]
α : Type u_1
β : Type u_2
n d✝ k N : ℕ
x : Fin n → ℕ
d : ℕ
a : Fin 0 → ℕ
⊢ ↑(map d) a = 0
[PROOFSTEP]
simp [map]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
a : Fin (n + 1) → ℕ
⊢ ↑(map d) a = a 0 + (∑ x : Fin n, a (Fin.succ x) * d ^ ↑x) * d
[PROOFSTEP]
simp [map, Fin.sum_univ_succ, _root_.pow_succ', ← mul_assoc, ← sum_mul]
[GOAL]
α : Type u_1
β : Type u_2
n d✝ k N : ℕ
x✝ : Fin n → ℕ
d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ ↑(map d) x ≤ ↑(map d) y
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
n d✝ k N : ℕ
x✝ : Fin n → ℕ
d : ℕ
x y : Fin n → ℕ
h : x ≤ y
⊢ ∑ i : Fin n, x i * d ^ ↑i ≤ ∑ i : Fin n, y i * d ^ ↑i
[PROOFSTEP]
exact sum_le_sum fun i _ => Nat.mul_le_mul_right _ <| h i
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
a : Fin (succ n) → ℕ
⊢ ↑(map d) a % d = a 0 % d
[PROOFSTEP]
rw [map_succ, Nat.add_mul_mod_self_right]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
⊢ ↑(map d) x₁ = ↑(map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [map_succ', map_succ', h.1, h.2]⟩
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
⊢ ↑(map d) x₁ = ↑(map d) x₂
[PROOFSTEP]
rw [map_succ', map_succ', h.1, h.2]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
[PROOFSTEP]
have : x₁ 0 = x₂ 0 := by rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ 0 = x₂ 0
[PROOFSTEP]
rw [← mod_eq_of_lt (hx₁ _), ← map_mod, ← mod_eq_of_lt (hx₂ _), ← map_mod, h]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ↑(map d) x₁ = ↑(map d) x₂
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
[PROOFSTEP]
rw [map_succ, map_succ, this, add_right_inj, mul_eq_mul_right_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
x₁ x₂ : Fin (succ n) → ℕ
hx₁ : ∀ (i : Fin (succ n)), x₁ i < d
hx₂ : ∀ (i : Fin (succ n)), x₂ i < d
h : ∑ x : Fin n, x₁ (Fin.succ x) * d ^ ↑x = ∑ x : Fin n, x₂ (Fin.succ x) * d ^ ↑x ∨ d = 0
this : x₁ 0 = x₂ 0
⊢ x₁ 0 = x₂ 0 ∧ ↑(map d) (x₁ ∘ Fin.succ) = ↑(map d) (x₂ ∘ Fin.succ)
[PROOFSTEP]
exact ⟨this, h.resolve_right (pos_of_gt (hx₁ 0)).ne'⟩
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ Set.InjOn ↑(map d) {x | ∀ (i : Fin n), x i < d}
[PROOFSTEP]
intro x₁ hx₁ x₂ hx₂ h
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x x₁ : Fin n → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin n), x i < d}
x₂ : Fin n → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin n), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ = x₂
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ x₁✝ : Fin n → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n), x i < d}
x₂✝ : Fin n → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
x x₁ : Fin zero → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin zero), x i < d}
x₂ : Fin zero → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin zero), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ = x₂
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x✝ x₁✝ : Fin n✝ → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
x₂✝ : Fin n✝ → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
n : ℕ
ih :
  ∀ {x : Fin n → ℕ} ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → ↑(map d) x₁ = ↑(map d) x₂ → x₁ = x₂
x x₁ : Fin (succ n) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
x₂ : Fin (succ n) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ = x₂
[PROOFSTEP]
rw [forall_const] at ih
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x✝ x₁✝ : Fin n✝ → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
x₂✝ : Fin n✝ → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → ↑(map d) x₁ = ↑(map d) x₂ → x₁ = x₂
x x₁ : Fin (succ n) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
x₂ : Fin (succ n) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
⊢ x₁ = x₂
[PROOFSTEP]
ext i
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x✝ x₁✝ : Fin n✝ → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
x₂✝ : Fin n✝ → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → ↑(map d) x₁ = ↑(map d) x₂ → x₁ = x₂
x x₁ : Fin (succ n) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
x₂ : Fin (succ n) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
i : Fin (succ n)
⊢ x₁ i = x₂ i
[PROOFSTEP]
have x := (map_eq_iff hx₁ hx₂).1 h
[GOAL]
case succ.h
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x✝¹ x₁✝ : Fin n✝ → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
x₂✝ : Fin n✝ → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → ↑(map d) x₁ = ↑(map d) x₂ → x₁ = x₂
x✝ x₁ : Fin (succ n) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
x₂ : Fin (succ n) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
i : Fin (succ n)
x : x₁ 0 = x₂ 0 ∧ ↑(map d) ((fun i => x₁ i) ∘ Fin.succ) = ↑(map d) ((fun i => x₂ i) ∘ Fin.succ)
⊢ x₁ i = x₂ i
[PROOFSTEP]
refine' Fin.cases x.1 (congr_fun <| ih (fun _ => _) (fun _ => _) x.2) i
[GOAL]
case succ.h.refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x✝² x₁✝ : Fin n✝ → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
x₂✝ : Fin n✝ → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → ↑(map d) x₁ = ↑(map d) x₂ → x₁ = x₂
x✝¹ x₁ : Fin (succ n) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
x₂ : Fin (succ n) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
i : Fin (succ n)
x : x₁ 0 = x₂ 0 ∧ ↑(map d) ((fun i => x₁ i) ∘ Fin.succ) = ↑(map d) ((fun i => x₂ i) ∘ Fin.succ)
x✝ : Fin n
⊢ x₁ (Fin.succ x✝) < d
[PROOFSTEP]
exact hx₁ _
[GOAL]
case succ.h.refine'_2
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x✝² x₁✝ : Fin n✝ → ℕ
hx₁✝ : x₁✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
x₂✝ : Fin n✝ → ℕ
hx₂✝ : x₂✝ ∈ {x | ∀ (i : Fin n✝), x i < d}
h✝ : ↑(map d) x₁✝ = ↑(map d) x₂✝
n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → ↑(map d) x₁ = ↑(map d) x₂ → x₁ = x₂
x✝¹ x₁ : Fin (succ n) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
x₂ : Fin (succ n) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (succ n)), x i < d}
h : ↑(map d) x₁ = ↑(map d) x₂
i : Fin (succ n)
x : x₁ 0 = x₂ 0 ∧ ↑(map d) ((fun i => x₁ i) ∘ Fin.succ) = ↑(map d) ((fun i => x₂ i) ∘ Fin.succ)
x✝ : Fin n
⊢ x₂ (Fin.succ x✝) < d
[PROOFSTEP]
exact hx₂ _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ AddSalemSpencer ↑(sphere n d k)
[PROOFSTEP]
set f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toFun := fun f => ((↑) : ℕ → ℝ) ∘ f
    map_zero' := funext fun _ => cast_zero
    map_add' := fun _ _ => funext fun _ => cast_add _ _ }
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toZeroHom := { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : Fin n → ℕ),
          ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } (x + x_1) =
            ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x +
              ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x_1) }
⊢ AddSalemSpencer ↑(sphere n d k)
[PROOFSTEP]
refine' AddSalemSpencer.of_image (f.toAddFreimanHom (sphere n d k : Set (Fin n → ℕ)) 2) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toZeroHom := { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : Fin n → ℕ),
          ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } (x + x_1) =
            ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x +
              ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x_1) }
⊢ Set.InjOn ↑(AddMonoidHom.toAddFreimanHom (↑(sphere n d k)) 2 f) ↑(sphere n d k)
[PROOFSTEP]
exact cast_injective.comp_left.injOn _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toZeroHom := { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : Fin n → ℕ),
          ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } (x + x_1) =
            ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x +
              ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x_1) }
⊢ AddSalemSpencer (↑(AddMonoidHom.toAddFreimanHom (↑(sphere n d k)) 2 f) '' ↑(sphere n d k))
[PROOFSTEP]
refine' (addSalemSpencer_sphere 0 <| Real.sqrt k).mono (Set.image_subset_iff.2 fun x => _)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toZeroHom := { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : Fin n → ℕ),
          ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } (x + x_1) =
            ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x +
              ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x_1) }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → x ∈ ↑(AddMonoidHom.toAddFreimanHom (↑(sphere n d k)) 2 f) ⁻¹' Metric.sphere 0 (Real.sqrt ↑k)
[PROOFSTEP]
rw [Set.mem_preimage, mem_sphere_zero_iff_norm]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) :=
  { toZeroHom := { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : Fin n → ℕ),
          ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } (x + x_1) =
            ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x +
              ZeroHom.toFun { toFun := fun f => Nat.cast ∘ f, map_zero' := (_ : (fun f => Nat.cast ∘ f) 0 = 0) } x_1) }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → ‖↑(AddMonoidHom.toAddFreimanHom (↑(sphere n d k)) 2 f) x‖ = Real.sqrt ↑k
[PROOFSTEP]
exact norm_of_mem_sphere
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ AddSalemSpencer ↑(image (↑(map (2 * d - 1))) (sphere n d k))
[PROOFSTEP]
rw [coe_image]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ AddSalemSpencer (↑(map (2 * d - 1)) '' ↑(sphere n d k))
[PROOFSTEP]
refine'
  @AddSalemSpencer.image _ (Fin n → ℕ) ℕ _ _ (sphere n d k) _ (map (2 * d - 1)) (map_injOn.mono _)
    addSalemSpencer_sphere
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ Fin n → ℕ
[PROOFSTEP]
exact x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}
[PROOFSTEP]
rw [Set.add_subset_iff]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ ∀ (x : Fin n → ℕ),
    x ∈ ↑(sphere n d k) → ∀ (y : Fin n → ℕ), y ∈ ↑(sphere n d k) → x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}
[PROOFSTEP]
rintro a ha b hb i
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
⊢ (a + b) i < 2 * d - 1
[PROOFSTEP]
have hai := mem_box.1 (sphere_subset_box ha) i
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
⊢ (a + b) i < 2 * d - 1
[PROOFSTEP]
have hbi := mem_box.1 (sphere_subset_box hb) i
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1
[PROOFSTEP]
rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ succ ((a + b) i + 1) ≤ d + d
[PROOFSTEP]
exact (add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
[PROOFSTEP]
rw [mem_box] at hx
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
[PROOFSTEP]
have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i => Nat.pow_le_pow_of_le_left (Nat.le_pred_of_lt (hx i)) _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
[PROOFSTEP]
exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [card_fin, smul_eq_mul])
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hx : ∀ (i : Fin n), x i < d
this : ∀ (i : Fin n), x i ^ 2 ≤ (d - 1) ^ 2
⊢ card univ • (d - 1) ^ 2 ≤ n * (d - 1) ^ 2
[PROOFSTEP]
rw [card_fin, smul_eq_mul]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ ∑ i : Fin n, d * (2 * d + 1) ^ ↑i = ((2 * d + 1) ^ n - 1) / 2
[PROOFSTEP]
refine' (Nat.div_eq_of_eq_mul_left zero_lt_two _).symm
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ (2 * d + 1) ^ n - 1 = (∑ i : Fin n, d * (2 * d + 1) ^ ↑i) * 2
[PROOFSTEP]
rw [← sum_range fun i => d * (2 * d + 1) ^ (i : ℕ), ← mul_sum, mul_right_comm, mul_comm d, ← geom_sum_mul_add,
  add_tsub_cancel_right, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
⊢ card (sphere n d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ n)
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ card (sphere zero d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ zero)
[PROOFSTEP]
dsimp
[GOAL]
case zero
α : Type u_1
β : Type u_2
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ card (sphere 0 d k) ≤ ↑rothNumberNat 1
[PROOFSTEP]
refine' (card_le_univ _).trans_eq _
[GOAL]
case zero
α : Type u_1
β : Type u_2
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = ↑rothNumberNat 1
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k n✝ : ℕ
⊢ card (sphere (succ n✝) d k) ≤ ↑rothNumberNat ((2 * d - 1) ^ succ n✝)
[PROOFSTEP]
cases d
[GOAL]
case succ.zero
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝ : ℕ
⊢ card (sphere (succ n✝) zero k) ≤ ↑rothNumberNat ((2 * zero - 1) ^ succ n✝)
[PROOFSTEP]
simp
[GOAL]
case succ.succ
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ card (sphere (succ n✝¹) (succ n✝) k) ≤ ↑rothNumberNat ((2 * succ n✝ - 1) ^ succ n✝¹)
[PROOFSTEP]
refine' addSalemSpencer_image_sphere.le_rothNumberNat _ _ (card_image_of_injOn _)
[GOAL]
case succ.succ.refine'_1
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Fin (succ n✝¹) → ℕ
[PROOFSTEP]
intro
[GOAL]
case succ.succ.refine'_1
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
a✝ : Fin (succ n✝¹)
⊢ ℕ
[PROOFSTEP]
assumption
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ), x ∈ image (↑(map (2 * succ n✝ - 1))) (sphere (succ n✝¹) (succ n✝) k) → x < (2 * succ n✝ - 1) ^ succ n✝¹
[PROOFSTEP]
simp only [subset_iff, mem_image, and_imp, forall_exists_index, mem_range, forall_apply_eq_imp_iff₂, sphere, mem_filter]
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ) (x_1 : Fin (succ n✝¹) → ℕ),
    x_1 ∈ box (succ n✝¹) (succ n✝) →
      ∑ i : Fin (succ n✝¹), x_1 i ^ 2 = k → ↑(map (2 * succ n✝ - 1)) x_1 = x → x < (2 * succ n✝ - 1) ^ succ n✝¹
[PROOFSTEP]
rintro _ x hx _ rfl
[GOAL]
case succ.succ.refine'_2
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
hx : x ∈ box (succ n✝¹) (succ n✝)
a✝ : ∑ i : Fin (succ n✝¹), x i ^ 2 = k
⊢ ↑(map (2 * succ n✝ - 1)) x < (2 * succ n✝ - 1) ^ succ n✝¹
[PROOFSTEP]
exact (map_le_of_mem_box hx).trans_lt sum_lt
[GOAL]
case succ.succ.refine'_3
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Set.InjOn ↑(map (2 * succ n✝ - 1)) ↑(sphere (succ n✝¹) (succ n✝) k)
[PROOFSTEP]
refine' map_injOn.mono fun x => _
[GOAL]
case succ.succ.refine'_3.refine'_1
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
⊢ Fin (succ n✝¹) → ℕ
[PROOFSTEP]
intro
[GOAL]
case succ.succ.refine'_3.refine'_1
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x : Fin n → ℕ
k n✝¹ n✝ : ℕ
a✝ : Fin (succ n✝¹)
⊢ ℕ
[PROOFSTEP]
assumption
[GOAL]
case succ.succ.refine'_3.refine'_2
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
⊢ x ∈ ↑(sphere (succ n✝¹) (succ n✝) k) → x ∈ {x | ∀ (i : Fin (succ n✝¹)), x i < 2 * succ n✝ - 1}
[PROOFSTEP]
simp only [mem_coe, sphere, mem_filter, mem_box, and_imp, two_mul]
[GOAL]
case succ.succ.refine'_3.refine'_2
α : Type u_1
β : Type u_2
n d k✝ N : ℕ
x✝ : Fin n → ℕ
k n✝¹ n✝ : ℕ
x : Fin (succ n✝¹) → ℕ
⊢ (∀ (i : Fin (succ n✝¹)), x i < succ n✝) →
    ∑ i : Fin (succ n✝¹), x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (succ n✝¹)), x i < succ n✝ + succ n✝ - 1}
[PROOFSTEP]
exact fun h _ i => (h i).trans_le le_self_add
[GOAL]
α : Type u_1
β : Type u_2
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ∃ k, k ∈ range (n * (d - 1) ^ 2 + 1) ∧ ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
refine' exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => _) nonempty_range_succ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n✝ d✝ k N : ℕ
x✝ : Fin n✝ → ℕ
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)
[PROOFSTEP]
rw [mem_range, lt_succ_iff]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n✝ d✝ k N : ℕ
x✝ : Fin n✝ → ℕ
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2
[PROOFSTEP]
exact sum_sq_le_of_mem_box hx
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ card (range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(card (box n d))
[PROOFSTEP]
rw [card_range, _root_.nsmul_eq_mul, mul_div_assoc', cast_add_one, mul_div_cancel_left, card_box]
[GOAL]
case refine'_2.ha
α : Type u_1
β : Type u_2
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ↑(n * (d - 1) ^ 2) + 1 ≠ 0
[PROOFSTEP]
exact (cast_add_one_pos _).ne'
[GOAL]
α : Type u_1
β : Type u_2
n✝ d✝ k N : ℕ
x : Fin n✝ → ℕ
n d : ℕ
⊢ ∃ k, ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
⊢ ∃ k, ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
refine' ⟨k, _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
obtain rfl | hn := n.eq_zero_or_pos
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
n d✝ k✝ N : ℕ
x : Fin n → ℕ
d k : ℕ
hk : ↑(d ^ 0) / (↑(0 * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere 0 d k))
⊢ ↑d ^ ↑0 / ↑(0 * d ^ 2) ≤ ↑(card (sphere 0 d k))
[PROOFSTEP]
simp
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
obtain rfl | hd := d.eq_zero_or_pos
[GOAL]
case intro.intro.inr.inl
α : Type u_1
β : Type u_2
n✝ d k✝ N : ℕ
x : Fin n✝ → ℕ
n k : ℕ
hn : n > 0
hk : ↑(0 ^ n) / (↑(n * (0 - 1) ^ 2) + 1) ≤ ↑(card (sphere n 0 k))
⊢ ↑0 ^ ↑n / ↑(n * 0 ^ 2) ≤ ↑(card (sphere n 0 k))
[PROOFSTEP]
simp
[GOAL]
case intro.intro.inr.inr
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑d ^ ↑n / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
rw [rpow_nat_cast, ← cast_pow]
[GOAL]
case intro.intro.inr.inr
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(d ^ n) / ↑(n * d ^ 2) ≤ ↑(card (sphere n d k))
[PROOFSTEP]
refine' (div_le_div_of_le_left _ _ _).trans hk
[GOAL]
case intro.intro.inr.inr.refine'_1
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 ≤ ↑(d ^ n)
[PROOFSTEP]
exact cast_nonneg _
[GOAL]
case intro.intro.inr.inr.refine'_2
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 0 < ↑(n * (d - 1) ^ 2) + 1
[PROOFSTEP]
exact cast_add_one_pos _
[GOAL]
case intro.intro.inr.inr.refine'_3
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ ↑(n * (d - 1) ^ 2) + 1 ≤ ↑(n * d ^ 2)
[PROOFSTEP]
simp only [← le_sub_iff_add_le', cast_mul, ← mul_sub, cast_pow, cast_sub hd, sub_sq, one_pow, cast_one, mul_one,
  sub_add, sub_sub_self]
[GOAL]
case intro.intro.inr.inr.refine'_3
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n * (2 * ↑d - 1)
[PROOFSTEP]
apply one_le_mul_of_one_le_of_one_le
[GOAL]
case intro.intro.inr.inr.refine'_3.ha
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ ↑n
[PROOFSTEP]
rwa [one_le_cast]
[GOAL]
case intro.intro.inr.inr.refine'_3.hb
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d - 1
[PROOFSTEP]
rw [_root_.le_sub_iff_add_le]
[GOAL]
case intro.intro.inr.inr.refine'_3.hb
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 + 1 ≤ 2 * ↑d
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro.inr.inr.refine'_3.hb
α : Type u_1
β : Type u_2
n✝ d✝ k✝ N : ℕ
x : Fin n✝ → ℕ
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(card (sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ d
[PROOFSTEP]
exact one_le_cast.2 hd
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (↑n - 2) / ↑n ≤ ↑(↑rothNumberNat ((2 * d - 1) ^ n))
[PROOFSTEP]
convert bound_aux' n d using 1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (↑n - 2) / ↑n = ↑d ^ ↑n / ↑(n * d ^ 2)
[PROOFSTEP]
rw [cast_mul, cast_pow, mul_comm, ← div_div, ← cast_two, ← cast_sub hn, rpow_nat_cast, rpow_nat_cast,
  pow_sub₀ _ (cast_ne_zero.2 hd) hn, ← div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ log 2 * 2 ≤ Real.sqrt (log 8)
[PROOFSTEP]
have : (8 : ℝ) = 2 ^ ((3 : ℕ) : ℝ) := by rw [rpow_nat_cast]; norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 = 2 ^ ↑3
[PROOFSTEP]
rw [rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 = 2 ^ 3
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ Real.sqrt (log 8)
[PROOFSTEP]
rw [this, log_rpow zero_lt_two (3 : ℕ)]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ≤ Real.sqrt (↑3 * log 2)
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ (log 2 * 2) ^ 2 ≤ ↑3 * log 2
[PROOFSTEP]
rw [mul_pow, sq (log 2), mul_assoc, mul_comm]
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 * log 2 ≤ ↑3 * log 2
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two)
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 * 2 ^ 2 ≤ ↑3
[PROOFSTEP]
rw [← le_div_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ log 2 ≤ ↑3 / 2 ^ 2
case h α : Type u_1 β : Type u_2 n d k N : ℕ x : Fin n → ℕ this : 8 = 2 ^ ↑3 ⊢ 0 < 2 ^ 2
[PROOFSTEP]
apply log_two_lt_d9.le.trans
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2
case h α : Type u_1 β : Type u_2 n d k N : ℕ x : Fin n → ℕ this : 8 = 2 ^ ↑3 ⊢ 0 < 2 ^ 2
[PROOFSTEP]
all_goals norm_num1
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0.6931471808 ≤ ↑3 / 2 ^ 2
[PROOFSTEP]
norm_num1
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 8 = 2 ^ ↑3
⊢ 0 < 2 ^ 2
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 2 / (1 - 2 / exp 1) ≤ 8
[PROOFSTEP]
rw [div_le_iff, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff (exp_pos _)]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 8 * 2 ≤ (8 - 2) * exp 1
[PROOFSTEP]
have : 16 < 6 * (2.7182818283 : ℝ) := by norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 16 < 6 * 2.7182818283
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 16 < 6 * 2.7182818283
⊢ 8 * 2 ≤ (8 - 2) * exp 1
[PROOFSTEP]
linarith [exp_one_gt_d9]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 1 - 2 / exp 1
[PROOFSTEP]
rw [sub_pos, div_lt_one]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 2 < exp 1
[PROOFSTEP]
exact exp_one_gt_d9.trans' (by norm_num)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 2 < 2.7182818283
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < exp 1
[PROOFSTEP]
exact exp_one_gt_d9.trans' (by norm_num)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 2.7182818283
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
have : ((12 : ℕ) : ℝ) * log 2 ≤ log N :=
  by
  rw [← log_rpow zero_lt_two, log_le_log, rpow_nat_cast]
  · norm_num1
    exact_mod_cast hN
  · exact rpow_pos_of_pos zero_lt_two _
  rw [cast_pos]
  exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N
[PROOFSTEP]
rw [← log_rpow zero_lt_two, log_le_log, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 4096 ≤ ↑N
[PROOFSTEP]
exact_mod_cast hN
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ ↑12
[PROOFSTEP]
exact rpow_pos_of_pos zero_lt_two _
[GOAL]
case h₁
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
[PROOFSTEP]
rw [cast_pos]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
refine'
  (mul_le_mul_of_nonneg_right ((log_le_log _ <| by norm_num1).2 two_div_one_sub_two_div_e_le_eight) <| by
        norm_num1).trans
    _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 8
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 ≤ 69 / 50
[PROOFSTEP]
norm_num1
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 2 / (1 - 2 / exp 1)
[PROOFSTEP]
refine' div_pos zero_lt_two _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < 1 - 2 / exp 1
[PROOFSTEP]
rw [sub_pos, div_lt_one (exp_pos _)]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 < exp 1
[PROOFSTEP]
exact exp_one_gt_d9.trans_le' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 2 ≤ 2.7182818283
[PROOFSTEP]
norm_num1
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 * (69 / 50) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
have l8 : log 8 = (3 : ℕ) * log 2 := by
  rw [← log_rpow zero_lt_two, rpow_nat_cast]
  norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = ↑3 * log 2
[PROOFSTEP]
rw [← log_rpow zero_lt_two, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ log 8 = log (2 ^ 3)
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 8 * (69 / 50) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
rw [l8]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * log 2 * (69 / 50) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
apply le_sqrt_of_sq_le (le_trans _ this)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * log 2 * (69 / 50)) ^ 2 ≤ ↑12 * log 2
[PROOFSTEP]
rw [mul_right_comm, mul_pow, sq (log 2), ← mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 * log 2 ≤ ↑12 * log 2
[PROOFSTEP]
apply mul_le_mul_of_nonneg_right _ (log_nonneg one_le_two)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ (↑3 * (69 / 50)) ^ 2 * log 2 ≤ ↑12
[PROOFSTEP]
rw [← le_div_iff']
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ log 2 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2
[PROOFSTEP]
exact log_two_lt_d9.le.trans (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0.6931471808 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ 0 < (↑3 * (69 / 50)) ^ 2
[PROOFSTEP]
exact sq_pos_of_ne_zero _ (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
l8 : log 8 = ↑3 * log 2
⊢ ↑3 * (69 / 50) ≠ 0
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
[PROOFSTEP]
have h₁ := ceil_lt_add_one hx.le
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
[PROOFSTEP]
have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by
  rw [_root_.le_sub_iff_add_le]
  apply (add_le_add_left h₁.le _).trans_eq
  rw [← add_assoc, sub_add_cancel]
  linarith
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x ≤ 2 - ↑⌈x⌉₊
[PROOFSTEP]
rw [_root_.le_sub_iff_add_le]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x + ↑⌈x⌉₊ ≤ 2
[PROOFSTEP]
apply (add_le_add_left h₁.le _).trans_eq
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x + (x + 1) = 2
[PROOFSTEP]
rw [← add_assoc, sub_add_cancel]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 + 1 = 2
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
[PROOFSTEP]
refine' lt_of_le_of_lt _ (div_lt_div_of_lt_left (exp_pos _) (cast_pos.2 <| ceil_pos.2 hx) h₁)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) ≤ exp (2 - ↑⌈x⌉₊) / (x + 1)
[PROOFSTEP]
refine' le_trans _ (div_le_div_of_le_of_nonneg (exp_le_exp.2 h₂) <| add_nonneg hx.le zero_le_one)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) ≤ exp (1 - x) / (x + 1)
[PROOFSTEP]
rw [le_div_iff (add_pos hx zero_lt_one), ← le_div_iff' (exp_pos _), ← exp_sub, neg_mul, sub_neg_eq_add, two_mul,
  sub_add_add_cancel, add_comm _ x]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ exp (x + 1)
[PROOFSTEP]
refine' le_trans _ (add_one_le_exp_of_nonneg <| add_nonneg hx.le zero_le_one)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ x + 1 + 1
[PROOFSTEP]
exact le_add_of_nonneg_right zero_le_one
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ x / exp 1 < ↑⌊x / 2⌋₊
[PROOFSTEP]
apply lt_of_le_of_lt _ (sub_one_lt_floor _)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ x / exp 1 ≤ x / 2 - 1
[PROOFSTEP]
have : 0 < 1 - 2 / exp 1 := by
  rw [sub_pos, div_lt_one (exp_pos _)]
  exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 0 < 1 - 2 / exp 1
[PROOFSTEP]
rw [sub_pos, div_lt_one (exp_pos _)]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 2 < exp 1
[PROOFSTEP]
exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
⊢ 2 ≤ 2.7182818283
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ x / exp 1 ≤ x / 2 - 1
[PROOFSTEP]
rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ← div_eq_mul_one_div, mul_div_assoc',
  one_le_div, ← div_le_iff this]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
case hc
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 2 / (1 - 2 / exp 1) ≤ x
this : 0 < 1 - 2 / exp 1
⊢ 2 ≠ 0
[PROOFSTEP]
exact two_ne_zero
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ ↑⌈x⌉₊ < 1.38 * x
[PROOFSTEP]
refine' (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 0 ≤ 50 / 19
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x
[PROOFSTEP]
rw [← le_sub_iff_add_le', ← sub_one_mul]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1 ≤ (1.38 - 1) * x
[PROOFSTEP]
have : (1.38 : ℝ) = 69 / 50 := by norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
⊢ 1.38 = 69 / 50
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 1 ≤ (1.38 - 1) * x
[PROOFSTEP]
rwa [this, show (69 / 50 - 1 : ℝ) = (50 / 19)⁻¹ by norm_num1, ← div_eq_inv_mul, one_le_div]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 69 / 50 - 1 = (50 / 19)⁻¹
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 50 / 19 ≤ x
this : 1.38 = 69 / 50
⊢ 0 < 50 / 19
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 2 ≤ nValue N
[PROOFSTEP]
refine' succ_le_of_lt (lt_ceil.2 <| lt_sqrt_of_sq_lt _)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ ↑1 ^ 2 < log ↑N
[PROOFSTEP]
rw [cast_one, one_pow, lt_log_iff_exp_lt]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ exp 1 < ↑N
α : Type u_1 β : Type u_2 n d k N : ℕ x : Fin n → ℕ hN : 3 ≤ N ⊢ 0 < ↑N
[PROOFSTEP]
refine' lt_of_lt_of_le _ (cast_le.2 hN)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ exp 1 < ↑3
[PROOFSTEP]
exact exp_one_lt_d9.trans_le (by norm_num)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 2.7182818286 ≤ ↑3
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < ↑N
[PROOFSTEP]
rw [cast_pos]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 3 ≤ N
⊢ 0 < N
[PROOFSTEP]
exact (zero_lt_succ _).trans_le hN
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 3 ≤ nValue N
[PROOFSTEP]
rw [nValue, ← lt_iff_add_one_le, lt_ceil, cast_two]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 < Real.sqrt (log ↑N)
[PROOFSTEP]
apply lt_sqrt_of_sq_lt
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 2 < log ↑N
[PROOFSTEP]
have : (2 : ℝ) ^ ((6 : ℕ) : ℝ) ≤ N := by
  rw [rpow_nat_cast]
  exact (cast_le.2 hN).trans' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ ↑6 ≤ ↑N
[PROOFSTEP]
rw [rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N
[PROOFSTEP]
exact (cast_le.2 hN).trans' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑64
[PROOFSTEP]
norm_num1
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log ↑N
[PROOFSTEP]
apply lt_of_lt_of_le _ ((log_le_log (rpow_pos_of_pos zero_lt_two _) _).2 this)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 < log (2 ^ ↑6)
α : Type u_1 β : Type u_2 n d k N : ℕ x : Fin n → ℕ hN : 64 ≤ N this : 2 ^ ↑6 ≤ ↑N ⊢ 0 < ↑N
[PROOFSTEP]
rw [log_rpow zero_lt_two, ← div_lt_iff']
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 < log 2
[PROOFSTEP]
exact log_two_gt_d9.trans_le' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 2 ^ 2 / ↑6 ≤ 0.6931471803
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑6
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < ↑N
[PROOFSTEP]
rw [cast_pos]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 64 ≤ N
this : 2 ^ ↑6 ≤ ↑N
⊢ 0 < 64
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
⊢ 0 < dValue N
[PROOFSTEP]
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N
[PROOFSTEP]
rw [dValue, floor_pos, ← log_le_log zero_lt_one, log_one, log_div _ two_ne_zero, log_rpow hN₀, div_mul_eq_mul_div,
  one_mul, sub_nonneg, le_div_iff]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N
[PROOFSTEP]
have : (nValue N : ℝ) ≤ 2 * sqrt (log N) :=
  by
  apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
  rw [two_mul, add_le_add_iff_left]
  apply le_sqrt_of_sq_le
  rw [one_pow, le_log_iff_exp_le hN₀]
  exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
[PROOFSTEP]
apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ Real.sqrt (log ↑N) + 1 ≤ 2 * Real.sqrt (log ↑N)
[PROOFSTEP]
rw [two_mul, add_le_add_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ^ 2 ≤ log ↑N
[PROOFSTEP]
rw [one_pow, le_log_iff_exp_le hN₀]
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ exp 1 ≤ ↑N
[PROOFSTEP]
exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2.7182818286 ≤ ↑8
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * ↑(nValue N) ≤ log ↑N
[PROOFSTEP]
apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * (2 * Real.sqrt (log ↑N)) ≤ log ↑N
[PROOFSTEP]
rw [← mul_assoc, ← le_div_iff (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 2 * 2 ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
apply log_two_mul_two_le_sqrt_log_eight.trans
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ Real.sqrt (log 8) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
apply Real.sqrt_le_sqrt
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ log 8 ≤ log ↑N
[PROOFSTEP]
rw [log_le_log _ hN₀]
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 8 ≤ ↑N
[PROOFSTEP]
exact_mod_cast hN₃
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 0 < 8
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 1 < N
[PROOFSTEP]
exact hN₃.trans_lt' (by norm_num)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * Real.sqrt (log ↑N)
⊢ 1 < 8
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑(nValue N)
[PROOFSTEP]
exact cast_pos.2 (nValue_pos <| hN₃.trans' <| by norm_num)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2 ≤ 8
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (1 / ↑(nValue N)) ≠ 0
[PROOFSTEP]
exact (rpow_pos_of_pos hN₀ _).ne'
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (1 / ↑(nValue N)) / 2
[PROOFSTEP]
exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
[PROOFSTEP]
have : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N := Nat.pow_le_pow_of_le_left (Nat.sub_le _ _) _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N - 1) ^ nValue N ≤ N
[PROOFSTEP]
apply this.trans
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * dValue N) ^ nValue N ≤ N
[PROOFSTEP]
suffices ((2 * dValue N) ^ nValue N : ℝ) ≤ N by exact_mod_cast this
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this✝ : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
this : (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
⊢ (2 * dValue N) ^ nValue N ≤ N
[PROOFSTEP]
exact_mod_cast this
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
[PROOFSTEP]
suffices i : (2 * dValue N : ℝ) ≤ (N : ℝ) ^ (1 / nValue N : ℝ)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ (2 * ↑(dValue N)) ^ ↑(nValue N) ≤ ↑N
[PROOFSTEP]
apply (rpow_le_rpow (mul_nonneg zero_le_two (cast_nonneg _)) i (cast_nonneg _)).trans
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ (↑N ^ (1 / ↑(nValue N))) ^ ↑(nValue N) ≤ ↑N
[PROOFSTEP]
rw [← rpow_mul (cast_nonneg _), one_div_mul_cancel, rpow_one]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ ↑(nValue N) ≠ 0
[PROOFSTEP]
rw [cast_ne_zero]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
i : 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
⊢ nValue N ≠ 0
[PROOFSTEP]
apply (nValue_pos hN).ne'
[GOAL]
case i
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 2 * ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N))
[PROOFSTEP]
rw [← le_div_iff']
[GOAL]
case i
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ ↑(dValue N) ≤ ↑N ^ (1 / ↑(nValue N)) / 2
[PROOFSTEP]
exact floor_le (div_nonneg (rpow_nonneg_of_nonneg (cast_nonneg _) _) zero_le_two)
[GOAL]
case i
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N
⊢ 0 < 2
[PROOFSTEP]
apply zero_lt_two
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑N ^ (1 / ↑(nValue N)) / exp 1 < ↑(dValue N)
[PROOFSTEP]
apply div_lt_floor _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 / (1 - 2 / exp 1) ≤ ↑N ^ (1 / ↑(nValue N))
[PROOFSTEP]
rw [← log_le_log, log_rpow, mul_comm, ← div_eq_mul_one_div]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) ≤ log ↑N / ↑(nValue N)
[PROOFSTEP]
apply le_trans _ (div_le_div_of_le_left _ _ (ceil_lt_mul _).le)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) ≤ log ↑N / (1.38 * Real.sqrt (log ↑N))
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈Real.sqrt (log ↑N)⌉₊
α : Type u_1 β : Type u_2 n d k N : ℕ x : Fin n → ℕ hN : 4096 ≤ N ⊢ 50 / 19 ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
rw [mul_comm, ← div_div, div_sqrt, le_div_iff]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * 1.38 ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / exp 1)) * (69 / 50) ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
exact le_sqrt_log hN
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 1.38
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 ≤ log ↑N
[PROOFSTEP]
apply log_nonneg
[GOAL]
case hx
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ ↑N
[PROOFSTEP]
rw [one_le_cast]
[GOAL]
case hx
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ N
[PROOFSTEP]
exact hN.trans' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈Real.sqrt (log ↑N)⌉₊
[PROOFSTEP]
rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < log ↑N
[PROOFSTEP]
refine' log_pos _
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < ↑N
[PROOFSTEP]
rw [one_lt_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 1 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ Real.sqrt (log ↑N)
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ (50 / 19) ^ 2 ≤ log ↑N
[PROOFSTEP]
have : ((12 : ℕ) : ℝ) * log 2 ≤ log N :=
  by
  rw [← log_rpow zero_lt_two, log_le_log, rpow_nat_cast]
  · norm_num1
    exact_mod_cast hN
  · exact rpow_pos_of_pos zero_lt_two _
  rw [cast_pos]
  exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑12 * log 2 ≤ log ↑N
[PROOFSTEP]
rw [← log_rpow zero_lt_two, log_le_log, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ^ 12 ≤ ↑N
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 4096 ≤ ↑N
[PROOFSTEP]
exact_mod_cast hN
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 ^ ↑12
[PROOFSTEP]
exact rpow_pos_of_pos zero_lt_two _
[GOAL]
case h₁
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
[PROOFSTEP]
rw [cast_pos]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ log ↑N
[PROOFSTEP]
refine' le_trans _ this
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2
[PROOFSTEP]
rw [← div_le_iff']
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2
[PROOFSTEP]
exact log_two_gt_d9.le.trans' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ 0.6931471803
[PROOFSTEP]
norm_num1
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12
[PROOFSTEP]
norm_num1
[GOAL]
case hx
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
[PROOFSTEP]
rw [cast_pos]
[GOAL]
case hx
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / exp 1)
[PROOFSTEP]
refine' div_pos zero_lt_two _
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 1 - 2 / exp 1
[PROOFSTEP]
rw [sub_pos, div_lt_one (exp_pos _)]
[GOAL]
case h
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 < exp 1
[PROOFSTEP]
exact lt_of_le_of_lt (by norm_num1) exp_one_gt_d9
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 2 ≤ 2.7182818283
[PROOFSTEP]
norm_num1
[GOAL]
case h₁
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (1 / ↑(nValue N))
[PROOFSTEP]
apply rpow_pos_of_pos
[GOAL]
case h₁.hx
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N
[PROOFSTEP]
rw [cast_pos]
[GOAL]
case h₁.hx
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ 0 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 4096 ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
let n := nValue N
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
have hn : 0 < (n : ℝ) := cast_pos.2 (nValue_pos <| hN.trans' <| by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
⊢ 2 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
⊢ 8 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
⊢ succ 0 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
have hn₂ : 2 ≤ n := two_le_nValue (hN.trans' <| by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
⊢ 3 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
⊢ 2 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(↑rothNumberNat N)
[PROOFSTEP]
refine' ((bound_aux hd.ne' hn₂).trans <| cast_le.2 <| rothNumberNat.mono this).trans_lt' _
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(dValue N) ^ (↑n - 2) / ↑n
[PROOFSTEP]
conv_rhs => rw [← cast_two, ← cast_sub hn₂, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
| ↑(dValue N) ^ (↑n - 2) / ↑n
[PROOFSTEP]
rw [← cast_two, ← cast_sub hn₂, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
| ↑(dValue N) ^ (↑n - 2) / ↑n
[PROOFSTEP]
rw [← cast_two, ← cast_sub hn₂, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
| ↑(dValue N) ^ (↑n - 2) / ↑n
[PROOFSTEP]
rw [← cast_two, ← cast_sub hn₂, rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) < ↑(dValue N) ^ (n - 2) / ↑n
[PROOFSTEP]
refine' (div_lt_div_of_lt hn <| pow_lt_pow_of_lt_left (bound hN) _ _).trans_le' _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 0 ≤ ↑N ^ (1 / ↑(nValue N)) / exp 1
[PROOFSTEP]
exact div_nonneg (rpow_nonneg_of_nonneg (cast_nonneg _) _) (exp_pos _).le
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 0 < n - 2
[PROOFSTEP]
exact tsub_pos_of_lt (three_le_nValue <| hN.trans' <| by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ 64 ≤ 4096
[PROOFSTEP]
norm_num1
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ (↑N ^ (1 / ↑(nValue N)) / exp 1) ^ (n - 2) / ↑n
[PROOFSTEP]
rw [← rpow_nat_cast, div_rpow (rpow_nonneg_of_nonneg hN₀.le _) (exp_pos _).le, ← rpow_mul hN₀.le, mul_comm (_ / _),
  mul_one_div, cast_sub hn₂, cast_two, same_sub_div hn.ne', exp_one_rpow, div_div, rpow_sub hN₀, rpow_one, div_div,
  div_eq_mul_inv]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N * (↑N ^ (2 / ↑n) * (exp (↑n - 2) * ↑n))⁻¹
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left _ (cast_nonneg _)
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ (↑N ^ (2 / ↑n) * (exp (↑n - 2) * ↑n))⁻¹
[PROOFSTEP]
rw [mul_inv, mul_inv, ← exp_neg, ← rpow_neg (cast_nonneg _), neg_sub, ← div_eq_mul_inv]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
[PROOFSTEP]
have : exp (-4 * sqrt (log N)) = exp (-2 * sqrt (log N)) * exp (-2 * sqrt (log N)) :=
  by
  rw [← exp_add, ← add_mul]
  norm_num
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
[PROOFSTEP]
rw [← exp_add, ← add_mul]
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ exp (-4 * Real.sqrt (log ↑N)) = exp ((-2 + -2) * Real.sqrt (log ↑N))
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-4 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n)) * (exp (2 - ↑n) / ↑n)
[PROOFSTEP]
refine'
  mul_le_mul _ (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos _).le (exp_pos _).le <|
    rpow_nonneg_of_nonneg (cast_nonneg _) _
[GOAL]
case refine'_3.refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ exp (-2 * Real.sqrt (log ↑N)) ≤ ↑N ^ (-(2 / ↑n))
[PROOFSTEP]
rw [← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _), log_rpow hN₀, ← le_div_iff, mul_div_assoc, div_sqrt, neg_mul,
  neg_le_neg_iff, div_mul_eq_mul_div, div_le_iff hn]
[GOAL]
case refine'_3.refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 2 * Real.sqrt (log ↑N) ≤ 2 * ↑n
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (le_ceil _) zero_le_two
[GOAL]
case refine'_3.refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 0 < Real.sqrt (log ↑N)
[PROOFSTEP]
refine' Real.sqrt_pos.2 (log_pos _)
[GOAL]
case refine'_3.refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < ↑N
[PROOFSTEP]
rw [one_lt_cast]
[GOAL]
case refine'_3.refine'_1
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
case refine'_3.refine'_2
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < ↑N
[PROOFSTEP]
rw [one_lt_cast]
[GOAL]
case refine'_3.refine'_2
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < N
[PROOFSTEP]
exact hN.trans_lt' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n✝ d k N : ℕ
x : Fin n✝ → ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 ≤ n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : exp (-4 * Real.sqrt (log ↑N)) = exp (-2 * Real.sqrt (log ↑N)) * exp (-2 * Real.sqrt (log ↑N))
⊢ 1 < 4096
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ exp 4 < 64
[PROOFSTEP]
rw [show (64 : ℝ) = 2 ^ ((6 : ℕ) : ℝ) by rw [rpow_nat_cast]; norm_num1, ←
  lt_log_iff_exp_lt (rpow_pos_of_pos zero_lt_two _), log_rpow zero_lt_two, ← div_lt_iff']
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 64 = 2 ^ ↑6
[PROOFSTEP]
rw [rpow_nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 64 = 2 ^ 6
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 4 / ↑6 < log 2
α : Type u_1 β : Type u_2 n d k N : ℕ x : Fin n → ℕ ⊢ 0 < ↑6
[PROOFSTEP]
exact log_two_gt_d9.trans_le' (by norm_num1)
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 4 / ↑6 ≤ 0.6931471803
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < ↑6
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 4096 < exp 16
[PROOFSTEP]
rw [← log_lt_iff_lt_exp (show (0 : ℝ) < 4096 by norm_num), show (4096 : ℝ) = 2 ^ 12 by norm_cast, log_rpow zero_lt_two]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 0 < 4096
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 4096 = 2 ^ 12
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 12 * log 2 < 16
[PROOFSTEP]
have : 12 * (0.6931471808 : ℝ) < 16 := by norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ 12 * 0.6931471808 < 16
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
this : 12 * 0.6931471808 < 16
⊢ 12 * log 2 < 16
[PROOFSTEP]
linarith [log_two_lt_d9]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
[PROOFSTEP]
rw [← log_le_log (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one, log_one,
  log_mul (cast_pos.2 (zero_lt_two.trans_le hN)).ne' (exp_pos _).ne', log_exp, neg_mul, ← sub_eq_add_neg, sub_nonpos, ←
  div_le_iff (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| one_lt_two.trans_le hN), div_sqrt,
  sqrt_le_left zero_le_four, log_le_iff_le_exp (cast_pos.2 (zero_lt_two.trans_le hN))]
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ exp (4 ^ 2)
[PROOFSTEP]
norm_num1
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ exp 16
[PROOFSTEP]
apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ 4096
[PROOFSTEP]
exact_mod_cast hN'
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : 1 ≤ N
hN' : N ≤ 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
[PROOFSTEP]
obtain rfl | hN := hN.eq_or_lt
[GOAL]
case inl
α : Type u_1
β : Type u_2
n d k : ℕ
x : Fin n → ℕ
hN : 1 ≤ 1
hN' : 1 ≤ 4096
⊢ ↑1 * exp (-4 * Real.sqrt (log ↑1)) ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case inr
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN✝ : 1 ≤ N
hN' : N ≤ 4096
hN : 1 < N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ 1
[PROOFSTEP]
exact lower_bound_le_one' hN hN'
[GOAL]
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
[PROOFSTEP]
obtain rfl | hN := Nat.eq_zero_or_pos N
[GOAL]
case inl
α : Type u_1
β : Type u_2
n d k : ℕ
x : Fin n → ℕ
⊢ ↑0 * exp (-4 * Real.sqrt (log ↑0)) ≤ ↑(↑rothNumberNat 0)
[PROOFSTEP]
norm_num
[GOAL]
case inr
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
[PROOFSTEP]
obtain h₁ | h₁ := le_or_lt 4096 N
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
[PROOFSTEP]
exact (roth_lower_bound_explicit h₁).le
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : N < 4096
⊢ ↑N * exp (-4 * Real.sqrt (log ↑N)) ≤ ↑(↑rothNumberNat N)
[PROOFSTEP]
apply (lower_bound_le_one hN h₁.le).trans
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
n d k N : ℕ
x : Fin n → ℕ
hN : N > 0
h₁ : N < 4096
⊢ 1 ≤ ↑(↑rothNumberNat N)
[PROOFSTEP]
simpa using rothNumberNat.monotone hN


[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
cases' le_or_lt ε 0 with hε hε
[GOAL]
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall, min_eq_right (by linarith [hT.out] : 2 * ε ≤ T),
  ENNReal.ofReal_eq_zero]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ T
[PROOFSTEP]
linarith [hT.out]
[GOAL]
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0
[PROOFSTEP]
exact mul_nonpos_of_nonneg_of_nonpos zero_le_two hε
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
suffices volume (closedBall x ε) ≤ volume (ball x ε) by
  exact (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this measurableSet_ball (measure_ne_top _ _)).symm
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : ↑↑volume (closedBall x ε) ≤ ↑↑volume (ball x ε)
⊢ closedBall x ε =ᶠ[ae volume] ball x ε
[PROOFSTEP]
exact (ae_eq_of_subset_of_measure_ge ball_subset_closedBall this measurableSet_ball (measure_ne_top _ _)).symm
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ ↑↑volume (closedBall x ε) ≤ ↑↑volume (ball x ε)
[PROOFSTEP]
have : Tendsto (fun δ => volume (closedBall x δ)) (𝓝[<] ε) (𝓝 <| volume (closedBall x ε)) :=
  by
  simp_rw [volume_closedBall]
  refine' ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ _)
  convert (@monotone_id ℝ _).tendsto_nhdsWithin_Iio ε
  simp
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => ↑↑volume (closedBall x δ)) (𝓝[Iio ε] ε) (𝓝 (↑↑volume (closedBall x ε)))
[PROOFSTEP]
simp_rw [volume_closedBall]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ => ENNReal.ofReal (min T (2 * δ))) (𝓝[Iio ε] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))
[PROOFSTEP]
refine' ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ _)
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun k => k) (𝓝[Iio ε] ε) (𝓝 ε)
[PROOFSTEP]
convert (@monotone_id ℝ _).tendsto_nhdsWithin_Iio ε
[GOAL]
case h.e'_5.h.e'_3
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ ε = sSup (id '' Iio ε)
[PROOFSTEP]
simp
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => ↑↑volume (closedBall x δ)) (𝓝[Iio ε] ε) (𝓝 (↑↑volume (closedBall x ε)))
⊢ ↑↑volume (closedBall x ε) ≤ ↑↑volume (ball x ε)
[PROOFSTEP]
refine' le_of_tendsto this (mem_nhdsWithin_Iio_iff_exists_Ioo_subset.mpr ⟨0, hε, fun r hr => _⟩)
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
this : Tendsto (fun δ => ↑↑volume (closedBall x δ)) (𝓝[Iio ε] ε) (𝓝 (↑↑volume (closedBall x ε)))
r : ℝ
hr : r ∈ Ioo 0 ε
⊢ r ∈ {x_1 | (fun c => ↑↑volume (closedBall x c) ≤ ↑↑volume (ball x ε)) x_1}
[PROOFSTEP]
exact measure_mono (closedBall_subset_ball hr.2)
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
⊢ IsAddFundamentalDomain { x // x ∈ AddSubgroup.zmultiples u } I
[PROOFSTEP]
set G := AddSubgroup.zmultiples u
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
set n := addOrderOf u
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑n))
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
set B := ball x (T / (2 * n))
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
have hn : 1 ≤ (n : ℝ) := by norm_cast; linarith [addOrderOf_pos' hu]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ 1 ≤ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
⊢ 1 ≤ n
[PROOFSTEP]
linarith [addOrderOf_pos' hu]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ IsAddFundamentalDomain { x // x ∈ G } I
[PROOFSTEP]
refine' IsAddFundamentalDomain.mk_of_measure_univ_le _ _ _ _
[GOAL]
case refine'_1
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ NullMeasurableSet I
[PROOFSTEP]
exact measurableSet_ball.nullMeasurableSet.congr hI.symm
[GOAL]
case refine'_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : { x // x ∈ G }), g ≠ 0 → AEDisjoint volume (g +ᵥ I) I
[PROOFSTEP]
rintro ⟨g, hg⟩ hg'
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : { val := g, property := hg } ≠ 0
⊢ AEDisjoint volume ({ val := g, property := hg } +ᵥ I) I
[PROOFSTEP]
replace hg' : g ≠ 0
[GOAL]
case hg'
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : { val := g, property := hg } ≠ 0
⊢ g ≠ 0
[PROOFSTEP]
simpa only [Ne.def, AddSubgroup.mk_eq_zero_iff] using hg'
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume ({ val := g, property := hg } +ᵥ I) I
[PROOFSTEP]
change AEDisjoint volume (g +ᵥ I) I
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume (g +ᵥ I) I
[PROOFSTEP]
refine'
  AEDisjoint.congr (Disjoint.aedisjoint _) ((quasiMeasurePreserving_add_left volume (-g)).vadd_ae_eq_of_ae_eq g hI) hI
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ Disjoint (g +ᵥ B) B
[PROOFSTEP]
have hBg : g +ᵥ B = ball (g + x) (T / (2 * n)) := by
  rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ g +ᵥ B = ball (g + x) (T / (2 * ↑n))
[PROOFSTEP]
rw [add_comm g x, ← singleton_add_ball _ x g, add_ball, thickening_singleton]
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ Disjoint (g +ᵥ B) B
[PROOFSTEP]
rw [hBg]
[GOAL]
case refine'_2.mk
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ Disjoint (ball (g + x) (T / (2 * ↑n))) B
[PROOFSTEP]
apply ball_disjoint_ball
[GOAL]
case refine'_2.mk.h
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / (2 * ↑n) + T / (2 * ↑n) ≤ dist (g + x) x
[PROOFSTEP]
rw [dist_eq_norm, add_sub_cancel, div_mul_eq_div_div, ← add_div, ← add_div, add_self_div_two,
  div_le_iff' (by positivity : 0 < (n : ℝ)), ← nsmul_eq_mul]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ 0 < ↑n
[PROOFSTEP]
positivity
[GOAL]
case refine'_2.mk.h
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T ≤ n • ‖g‖
[PROOFSTEP]
refine'
  (le_add_order_smul_norm_of_isOfFinAddOrder (hu.of_mem_zmultiples hg) hg').trans (nsmul_le_nsmul (norm_nonneg g) _)
[GOAL]
case refine'_2.mk.h
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ addOrderOf g ≤ n
[PROOFSTEP]
exact Nat.le_of_dvd (addOrderOf_pos_iff.mpr hu) (addOrderOf_dvd_of_mem_zmultiples hg)
[GOAL]
case refine'_3
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ∀ (g : { x // x ∈ G }), QuasiMeasurePreserving ((fun x x_1 => x +ᵥ x_1) g)
[PROOFSTEP]
exact fun g => quasiMeasurePreserving_add_left (G := AddCircle T) volume g
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᶠ[ae volume] B
hn : 1 ≤ ↑n
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
replace hI := hI.trans closedBall_ae_eq_ball.symm
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
have hG_card : (Finset.univ : Finset G).card = n :=
  by
  show _ = addOrderOf u
  rw [add_order_eq_card_zmultiples', Nat.card_eq_fintype_card]; rfl
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ Finset.card Finset.univ = n
[PROOFSTEP]
show _ = addOrderOf u
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ Finset.card Finset.univ = addOrderOf u
[PROOFSTEP]
rw [add_order_eq_card_zmultiples', Nat.card_eq_fintype_card]
[GOAL]
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
⊢ Finset.card Finset.univ = Fintype.card { x // x ∈ AddSubgroup.zmultiples u }
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
hG_card : Finset.card Finset.univ = n
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ G }), ↑↑volume (g +ᵥ I)
[PROOFSTEP]
simp_rw [measure_vadd]
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
hG_card : Finset.card Finset.univ = n
⊢ ↑↑volume univ ≤ ∑' (g : { x // x ∈ AddSubgroup.zmultiples u }), ↑↑volume I
[PROOFSTEP]
rw [AddCircle.measure_univ, tsum_fintype, Finset.sum_const, measure_congr hI, volume_closedBall, ← ENNReal.ofReal_nsmul,
  mul_div, mul_div_mul_comm, div_self, one_mul, min_eq_right (div_le_self hT.out.le hn), hG_card, nsmul_eq_mul,
  mul_div_cancel' T (lt_of_lt_of_le zero_lt_one hn).ne.symm]
[GOAL]
case refine'_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᶠ[ae volume] closedBall x (T / (2 * ↑n))
this : Fintype { x // x ∈ G }
hG_card : Finset.card Finset.univ = n
⊢ 2 ≠ 0
[PROOFSTEP]
exact two_ne_zero
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
let G := AddSubgroup.zmultiples u
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
haveI : Fintype G := @Fintype.ofFinite _ hu.finite_zmultiples
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
have hsG : ∀ g : G, (g +ᵥ s : Set <| AddCircle T) =ᵐ[volume] s := by rintro ⟨y, hy⟩;
  exact (vadd_ae_eq_self_of_mem_zmultiples hs hy : _)
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
⊢ ∀ (g : { x // x ∈ G }), g +ᵥ s =ᶠ[ae volume] s
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
y : AddCircle T
hy : y ∈ G
⊢ { val := y, property := hy } +ᵥ s =ᶠ[ae volume] s
[PROOFSTEP]
exact (vadd_ae_eq_self_of_mem_zmultiples hs hy : _)
[GOAL]
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae volume] s
hI : I =ᶠ[ae volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype { x // x ∈ G }
hsG : ∀ (g : { x // x ∈ G }), g +ᵥ s =ᶠ[ae volume] s
⊢ ↑↑volume s = addOrderOf u • ↑↑volume (s ∩ I)
[PROOFSTEP]
rw [(isAddFundamentalDomain_of_ae_ball I u x hu hI).measure_eq_card_smul_of_vadd_ae_eq_self s hsG,
  add_order_eq_card_zmultiples' u, Nat.card_eq_fintype_card]