Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1969P6

module

public import Mathlib.Tactic
public import Mathlib.Analysis.Real.Sqrt

public section


/-!
# International Mathematical Olympiad 1969, Problem 6

Given real numbers x₁, x₂, y₁, y₂, z₁, z₂ satisfying x₁ > 0, x₂ > 0,
x₁y₁ > z₁², and x₂y₂ > z₂², prove that

  8 / ((x₁ + x₂)(y₁ + y₂) - (z₁ + z₂)²) ≤ 1 / (x₁y₁ - z₁²) + 1 / (x₂y₂ - z₂²).

Give necessary and sufficient conditions for equality.
-/

namespace Imo1969P6

/-- The condition for equality to hold. -/
/- determine -/ abbrev eqCondition (x₁ x₂ y₁ y₂ z₁ z₂ : ℝ) : Prop := sorry

theorem imo1969_p6 (x₁ x₂ y₁ y₂ z₁ z₂ : ℝ)
    (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (h₁ : z₁ ^ 2 < x₁ * y₁) (h₂ : z₂ ^ 2 < x₂ * y₂) :
    8 / ((x₁ + x₂) * (y₁ + y₂) - (z₁ + z₂) ^ 2) ≤
        1 / (x₁ * y₁ - z₁ ^ 2) + 1 / (x₂ * y₂ - z₂ ^ 2) ∧
      (8 / ((x₁ + x₂) * (y₁ + y₂) - (z₁ + z₂) ^ 2) =
          1 / (x₁ * y₁ - z₁ ^ 2) + 1 / (x₂ * y₂ - z₂ ^ 2) ↔
        eqCondition x₁ x₂ y₁ y₂ z₁ z₂) := sorry

end Imo1969P6

File author(s): Kimi K3

This problem has a complete formalized solution.