[Imo1968P5] the constant of periodicity must be positive

dwrensha · Nov 20, 2023 · 2d18d49 · 2d18d49
1 parent 9b42716
commit 2d18d49
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Compfiles/Imo1968P5.lean b/Compfiles/Imo1968P5.lean
@@ -28,11 +28,12 @@ holds for all x.
 namespace Imo1968P5
 
 abbrev P (a : ℝ) (f : ℝ → ℝ) : Prop :=
-  ∀ x, f (x + a) = 1/2 + Real.sqrt (f x - (f x)^2)
+  0 < a ∧ ∀ x, f (x + a) = 1/2 + Real.sqrt (f x - (f x)^2)
 
 determine solution_func : ℝ → ℝ := sorry
 
-problem imo1968_p5a (f : ℝ → ℝ) (a : ℝ) (hf : P a f) : ∃ b, f.Periodic b := by
+problem imo1968_p5a (f : ℝ → ℝ) (a : ℝ) (hf : P a f) :
+    ∃ b, 0 < b ∧ f.Periodic b := by
   sorry
 
 problem imo1968_p5b :