Jcost_anti_mono_on_unit_interval

proof body

Tactic-mode proof.

 200  have hx_ne : x ≠ 0 := ne_of_gt hx
 201  have hy_ne : y ≠ 0 := ne_of_gt hy
 202  rw [Cost.Jcost_eq_sq hx_ne, Cost.Jcost_eq_sq hy_ne]
 203  -- Goal: (y-1)²/(2y) ≤ (x-1)²/(2x)
 204  -- Equivalent: 2x · (y-1)² ≤ 2y · (x-1)²  (multiplying by 2xy > 0)
 205  rw [div_le_div_iff₀ (by linarith : (0:ℝ) < 2 * y) (by linarith : (0:ℝ) < 2 * x)]
 206  -- Goal: (y-1)² · (2*x) ≤ (x-1)² · (2*y)
 207  -- Both x, y are in (0, 1], so y-1 ≤ 0 and x-1 ≤ 0. Let a = 1-x ≥ 0, b = 1-y ≥ 0,
 208  -- then b ≤ a (since x ≤ y means 1-y ≤ 1-x).
 209  -- (y-1)² = b², (x-1)² = a², so we want 2x · b² ≤ 2y · a².
 210  -- Equivalently: x · b² ≤ y · a².
 211  -- Since b ≤ a and b² ≤ a², and x ≤ y, the product inequality follows.
 212  set a := 1 - x with ha_def
 213  set b := 1 - y with hb_def
 214  have ha_nn : 0 ≤ a := by linarith
 215  have hb_nn : 0 ≤ b := by linarith
 216  have hba : b ≤ a := by linarith
 217  have hxy' : x ≤ y := hxy
 218  have hsq_nn : (1 - y) ^ 2 = b ^ 2 := by rw [hb_def]
 219  have hsq_nn' : (1 - x) ^ 2 = a ^ 2 := by rw [ha_def]
 220  have hyy_eq : (y - 1) ^ 2 = b ^ 2 := by rw [show (y - 1) = -(1 - y) from by ring]; ring
 221  have hxx_eq : (x - 1) ^ 2 = a ^ 2 := by rw [show (x - 1) = -(1 - x) from by ring]; ring
 222  rw [hyy_eq, hxx_eq]
 223  -- Goal: b^2 * (2*x) ≤ a^2 * (2*y).
 224  -- Use: b ≤ a (both nonneg) ⇒ b^2 ≤ a^2; and x ≤ y. Then b^2 * x ≤ a^2 * y.
 225  have hb2_le_a2 : b ^ 2 ≤ a ^ 2 := by
 226    have := mul_self_le_mul_self hb_nn hba
 227    rw [pow_two, pow_two]; exact this
 228  have hb2_nn : 0 ≤ b ^ 2 := by positivity
 229  have ha2_nn : 0 ≤ a ^ 2 := by positivity
 230  -- b^2 · (2x) ≤ a^2 · (2x) ≤ a^2 · (2y).
 231  have step1 : b ^ 2 * (2 * x) ≤ a ^ 2 * (2 * x) :=
 232    mul_le_mul_of_nonneg_right hb2_le_a2 (by linarith)
 233  have step2 : a ^ 2 * (2 * x) ≤ a ^ 2 * (2 * y) :=
 234    mul_le_mul_of_nonneg_left (by linarith) ha2_nn
 235  linarith
 236
 237/-- **PREFERENCE ANTI-MONOTONICITY ON THE WALLPAPER LATTICE.** For two
 238wallpaper groups, the one with strictly more orbits has lower J-cost
 239(equivalently, higher preference). -/