eq_one_of_not_dvd — Mathlib

English

There exists a minimal natural p with properties 0<f(p)<1 and minimality condition.

Русский

Существует минимальное натуральное p с свойствами 0<f(p)<1 и условием минимальности.

LaTeX

$$∃ p, 0

Lean4

/-- A natural number not divisible by `p` has absolute value 1. -/
theorem eq_one_of_not_dvd {m : ℕ} (hpm : ¬p ∣ m) : f m = 1 :=
  by
  apply le_antisymm (bdd m)
  by_contra! hm
  set M := f p ⊔ f m with hM
  set k := Nat.ceil (M.logb (1 / 2)) + 1 with hk
  obtain ⟨a, b, bezout⟩ : IsCoprime (p ^ k : ℤ) (m ^ k) :=
    is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin |>.coprime_iff_not_dvd |>.mpr hpm |>.isCoprime |>.pow
  have le_half {x} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M) : x ^ k < 1 / 2 := by
    calc
      x ^ k = x ^ (k : ℝ) := (rpow_natCast x k).symm
      _ < x ^ M.logb (1 / 2) := by
        apply rpow_lt_rpow_of_exponent_gt hx0 hx1
        rw [hk]
        push_cast
        exact lt_add_of_le_of_pos (Nat.le_ceil _) zero_lt_one
      _ ≤ x ^ x.logb (1 / 2) := by
        apply rpow_le_rpow_of_exponent_ge hx0 hx1.le
        simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]
        gcongr
        simp only [Left.neg_pos_iff]
        exact log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)
      _ = 1 / 2 := rpow_logb hx0 hx1.ne one_half_pos
  apply lt_irrefl (1 : ℝ)
  calc
    1 = f 1 := (map_one f).symm
    _ = f (a * p ^ k + b * m ^ k) := by rw_mod_cast [bezout]; norm_cast
    _ ≤ f (a * p ^ k) + f (b * m ^ k) := f.add_le' ..
    _ ≤ 1 * (f p) ^ k + 1 * (f m) ^ k := by
      simp only [map_mul, map_pow]
      gcongr
      all_goals rw [← apply_natAbs_eq]; apply bdd
    _ = (f p) ^ k + (f m) ^ k := by simp only [one_mul]
    _ < 1 := by
      have hm₀ : 0 < f m := f.pos <| Nat.cast_ne_zero.mpr fun H ↦ hpm <| H ▸ dvd_zero p
      linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]
        -- ## Step 4: f p = p ^ (-t) for some positive real t

Похожие утверждения