internlm/Lean-Github huggingface dataset:
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_2.h₀
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∀ b ∈ P.divisors,
    b ≠ ∏ i : Fin k, a i → (if ∏ i : Fin k, a i = b ∧ b ∣ P then if ↑b ≤ x then (↑b)⁻¹ else 0 else 0) = 0
Tactic:
exact fun d _ hd_ne ↦ if_neg fun h => hd_ne.symm h.1
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_2.h₁
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∉ P.divisors →
    (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
        if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
      else 0) =
      0
Tactic:
exact fun h ↦ if_neg fun h' => h (mem_divisors.mpr ⟨h'.2, hP.ne_zero⟩)
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_3
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
apply sum_le_sum
Proof state after:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ∏ i_1 : Fin k, i i_1 ∣ P then if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0 else 0) ≤
      if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ∏ i_1 : Fin k, i i_1 ∣ P then if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0 else 0) ≤
      if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0
Tactic:
intro a _
Proof state after:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
by_cases h : (∏ i, a i ∣ P)
Proof state after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
rw [if_neg h]
Proof state after:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ 0 ≤ if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ 0 ≤ if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
split_ifs with h'
Proof state after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, (↑(a i))⁻¹

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
rw [if_pos h]
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, (↑(a i))⁻¹
Tactic:
apply prod_nonneg
Proof state after:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹
Tactic:
intro i _
Proof state after:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
a✝ : i ∈ univ
⊢ 0 ≤ (↑(a i))⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
a✝ : i ∈ univ
⊢ 0 ≤ (↑(a i))⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_4
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
apply sum_le_sum
Proof state after:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0) ≤
      ∏ i_1 : Fin k, if ↑(i i_1) ≤ x then (↑(i i_1))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0) ≤
      ∏ i_1 : Fin k, if ↑(i i_1) ≤ x then (↑(i i_1))⁻¹ else 0
Tactic:
intro a ha
Proof state after:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
split_ifs with h
Proof state after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∏ i : Fin k, (↑(a i))⁻¹ ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∏ i : Fin k, (↑(a i))⁻¹ ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
gcongr with i hi
Proof state after:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹

case pos.h1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ (↑(a i))⁻¹ ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos.h1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ (↑(a i))⁻¹ ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
rw [if_pos]
Proof state after:
case pos.h1.hc
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ x
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos.h1.hc
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ x
Tactic:
apply le_trans _ h
Proof state after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ ↑(∏ i : Fin k, a i)
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ ↑(∏ i : Fin k, a i)
Tactic:
norm_cast
Proof state after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ ∏ i : Fin k, a i
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ ∏ i : Fin k, a i
Tactic:
rw [←prod_erase_mul (a:=i) (h:= hi)]
Proof state after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ (∏ x ∈ univ.erase i, a x) * a i
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ (∏ x ∈ univ.erase i, a x) * a i
Tactic:
apply Nat.le_mul_of_pos_left
Proof state after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
Tactic:
rw [Fintype.mem_piFinset] at ha
Proof state after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
Tactic:
apply prod_pos
Proof state after:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ∀ i_1 ∈ univ.erase i, 0 < a i_1
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ∀ i_1 ∈ univ.erase i, 0 < a i_1
Tactic:
intro j _
Proof state after:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
j : Fin k
a✝ : j ∈ univ.erase i
⊢ 0 < a j
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
j : Fin k
a✝ : j ∈ univ.erase i
⊢ 0 < a j
Tactic:
apply pos_of_mem_divisors (ha j)
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
apply prod_nonneg
Proof state after:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
intro j _
Proof state after:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
⊢ 0 ≤ if ↑(a j) ≤ x then (↑(a j))⁻¹ else 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
⊢ 0 ≤ if ↑(a j) ≤ x then (↑(a j))⁻¹ else 0
Tactic:
split_ifs
Proof state after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ↑(a j) ≤ x
⊢ 0 ≤ (↑(a j))⁻¹

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ¬↑(a j) ≤ x
⊢ 0 ≤ 0
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ↑(a j) ≤ x
⊢ 0 ≤ (↑(a j))⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ¬↑(a j) ≤ x
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) ^ k ≤ (1 + x.log) ^ k
Tactic:
rw [←sum_filter]
Proof state after:
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹) ^ k ≤ (1 + x.log) ^ k
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹) ^ k ≤ (1 + x.log) ^ k
Tactic:
gcongr
Proof state after:
case calc_5.hab
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ 1 + x.log
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case calc_5.hab
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ 1 + x.log
Tactic:
trans (∑ d in Icc 1 (floor x), (d:ℝ)⁻¹)
Proof state after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹ ≤ 1 + x.log
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹ ≤ 1 + x.log
Tactic:
apply sum_inv_le_log_real
Proof state after:
case hy
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ 1 ≤ x
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case hy
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ 1 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹
Tactic:
apply sum_le_sum_of_subset_of_nonneg
Proof state after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ filter (fun d => ↑d ≤ x) P.divisors ⊆ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ filter (fun d => ↑d ≤ x) P.divisors ⊆ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
intro d
Proof state after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ filter (fun d => ↑d ≤ x) P.divisors → d ∈ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ filter (fun d => ↑d ≤ x) P.divisors → d ∈ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
rw[mem_filter, mem_Icc]
Proof state after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ P.divisors ∧ ↑d ≤ x → 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ P.divisors ∧ ↑d ≤ x → 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
intro hd
Proof state after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
constructor
Proof state after:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d

case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d
Tactic:
rw [Nat.succ_le]
Proof state after:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < d
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < d
Tactic:
exact pos_of_mem_divisors hd.1
Proof state after:
no goals
Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow
Proof state before:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ d ≤ ⌊x⌋₊
Tactic:
rw [le_floor_iff]
Proof state after:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ ↑d ≤ x

case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x