quarticLogComparison

formal source

  25open Real
  26
  27/-- The quartic-log comparison used as the counterexample. -/
  28noncomputable def quarticLogComparison : ComparisonOperator :=
  29  fun x y => (Real.log (x / y)) ^ (4 : Nat)
  30
  31/-- The continuous non-polynomial combiner associated to the quartic-log
  32comparison on the nonnegative range. -/
  33noncomputable def quarticCombiner (a b : ℝ) : ℝ :=
  34  2 * a + 2 * b + 12 * Real.sqrt (a * b)
  35
  36theorem quarticCombiner_symmetric :
  37    ∀ a b : ℝ, quarticCombiner a b = quarticCombiner b a := by
  38  intro a b
  39  unfold quarticCombiner
  40  rw [mul_comm a b]
  41  ring
  42
  43theorem quarticCombiner_nonneg_on_nonneg :
  44    ∀ a b : ℝ, 0 ≤ a → 0 ≤ b → 0 ≤ quarticCombiner a b := by
  45  intro a b ha hb
  46  unfold quarticCombiner
  47  have h2a : 0 ≤ 2 * a := by positivity
  48  have h2b : 0 ≤ 2 * b := by positivity
  49  have hsqrt : 0 ≤ 12 * Real.sqrt (a * b) := by positivity
  50  linarith
  51
  52/-- The square-root term in the quartic combiner cannot be represented by a
  53single bilinear coefficient `c*a*b` on all positive inputs. -/
  54theorem quartic_sqrt_term_not_bilinear :
  55    ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
  56      12 * Real.sqrt (a * b) = c * a * b := by
  57  intro h
  58  rcases h with ⟨c, hc⟩