kernel_match_pointwise

proof body

Tactic-mode proof.

  63  classical
  64  set y := 1 + 2 * Real.cot ϑ
  65  set s := Real.sqrt (y ^ 2 - 1)
  66  have hy : 1 ≤ y := by
  67    simpa [y] using arcosh_arg_ge_one ϑ hϑ
  68  have hy_pos : 0 < y := lt_of_lt_of_le zero_lt_one hy
  69  have hynonneg : 0 ≤ y := le_trans (by norm_num) hy
  70  have hrad_nonneg : 0 ≤ y ^ 2 - 1 := by
  71    have hsub : 0 ≤ y - 1 := sub_nonneg.mpr hy
  72    have hadd : 0 ≤ y + 1 := add_nonneg hynonneg (by norm_num)
  73    have hx := mul_nonneg hsub hadd
  74    convert hx using 1 <;> ring
  75  have hs_sq : s ^ 2 = y ^ 2 - 1 := by
  76    have := Real.mul_self_sqrt hrad_nonneg
  77    simpa [s, pow_two] using this
  78  have hxmul : (y + s) * (y - s) = 1 := by
  79    calc
  80      (y + s) * (y - s) = y ^ 2 - s ^ 2 := by ring
  81      _ = y ^ 2 - (y ^ 2 - 1) := by simpa [pow_two, hs_sq]
  82      _ = 1 := by ring
  83  have hxpos : 0 < y + s := add_pos_of_pos_of_nonneg hy_pos (Real.sqrt_nonneg _)
  84  have hxinv :
  85      (y + s) ⁻¹ = y - s := by
  86    have hxnonzero : y + s ≠ 0 := ne_of_gt hxpos
  87    have hx' := congrArg (fun t => (y + s)⁻¹ * t) hxmul
  88    have hx'' : (y - s) = (y + s)⁻¹ := by
  89      simpa [mul_assoc, hxnonzero] using hx'
  90    simpa [recognitionProfile, y, s] using hx''.symm
  91  have hxsum : (y + s) + (y - s) = 2 * y := by ring
  92  have hydiv : (2 * y) / 2 = y := by
  93    have : (2 : ℝ) ≠ 0 := by norm_num
  94    simpa [mul_comm] using (mul_div_cancel' y this)
  95  have hy_sub : y - 1 = 2 * Real.cot ϑ := by simp [y]
  96  calc
  97    Jcost (recognitionProfile ϑ)
  98        = ((y + s) + (y + s)⁻¹) / 2 - 1 := by simp [Jcost, recognitionProfile, y, s]
  99    _ = ((y + s) + (y - s)) / 2 - 1 := by simp [hxinv]
 100    _ = (2 * y) / 2 - 1 := by simpa [hxsum]
 101    _ = y - 1 := by simpa [hydiv]
 102    _ = 2 * Real.cot ϑ := hy_sub
 103
 104/-- Differential form of kernel match: J(r) dϑ = 2 tan ϑ dϑ -/