[Imo1968P5] intial steps

dwrensha · Nov 20, 2023 · 12c409a · 12c409a
1 parent 2d18d49
commit 12c409a
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/Compfiles/Imo1968P5.lean b/Compfiles/Imo1968P5.lean
@@ -34,6 +34,12 @@ determine solution_func : ℝ → ℝ := sorry
 
 problem imo1968_p5a (f : ℝ → ℝ) (a : ℝ) (hf : P a f) :
     ∃ b, 0 < b ∧ f.Periodic b := by
+  obtain ⟨hf1, hf2⟩ := hf
+  use 2 * a
+  constructor
+  · positivity
+  have h1 : ∀ x, 1 / 2 ≤ f (x + 1) := fun x ↦ by
+    sorry
   sorry
 
 problem imo1968_p5b :