English
Under certain structured hypotheses, MinSqFacAux(n, k) satisfies the MinSqFacProp relation.
Русский
При определенных структурированных гипотезах MinSqFacAux(n, k) удовлетворяет relation MinSqFacProp.
LaTeX
$$$MinSqFacAux\\_has\\_prop(n,k,...)\\Rightarrow MinSqFacProp(n, MinSqFacAux(n,k))$$$
Lean4
theorem minSqFacAux_has_prop {n : ℕ} (k) (n0 : 0 < n) (i) (e : k = 2 * i + 3) (ih : ∀ m, Prime m → m ∣ n → k ≤ m) :
MinSqFacProp n (minSqFacAux n k) := by
rw [minSqFacAux]
by_cases h : n < k * k <;> simp only [h, ↓reduceDIte]
· refine squarefree_iff_prime_squarefree.2 fun p pp d => ?_
have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
have := Nat.mul_le_mul this this
exact not_le_of_gt h (le_trans this (le_of_dvd n0 d))
have k2 : 2 ≤ k := by omega
have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) :=
by
intro n' nd' nk
have hn' := le_of_dvd n0 nd'
refine
have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k := lt_of_le_of_lt (by gcongr) (Nat.minFac_lemma n k h)
@minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1) (by simp [e, left_distrib]) fun m m2 d => ?_
rcases Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me | ml
· subst me
contradiction
apply (Nat.eq_or_lt_of_le ml).resolve_left
intro me
rw [← me, e] at d
change 2 * (i + 2) ∣ n' at d
have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
rw [e] at this
exact absurd this (by cutsat)
have pk : k ∣ n → Prime k :=
by
refine fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) ?_⟩
exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
split_ifs with dk dkk
· exact ⟨pk dk, (Nat.dvd_div_iff_mul_dvd dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
· specialize IH (n / k) (div_dvd_of_dvd dk) dkk
exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff_mul_dvd dk).2 dkk) IH
· exact IH n (dvd_refl _) dk
termination_by n.sqrt + 2 - k
