arcosh_arg_ge_one

formal source

  24  1 + 2 * Real.cot ϑ + Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1)
  25
  26/-- The argument to arcosh is at least 1 for ϑ ∈ [0, π/2] -/
  27lemma arcosh_arg_ge_one (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  28  1 ≤ 1 + 2 * Real.cot ϑ := by
  29  have hsin : 0 ≤ Real.sin ϑ := by
  30    have hmem : ϑ ∈ Set.Icc (0 : ℝ) Real.pi := by
  31      constructor
  32      · exact hϑ.1
  33      · have hpi2_le_pi : (Real.pi / 2 : ℝ) ≤ Real.pi := by nlinarith [Real.pi_pos]
  34        exact le_trans hϑ.2 hpi2_le_pi
  35    simpa using Real.sin_nonneg_of_mem_Icc hmem
  36  have hcos : 0 ≤ Real.cos ϑ := by
  37    have hmem : ϑ ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) := by
  38      constructor
  39      · have hneg : (-(Real.pi / 2) : ℝ) ≤ 0 := by nlinarith [Real.pi_pos]
  40        exact le_trans hneg hϑ.1
  41      · exact hϑ.2
  42    simpa using Real.cos_nonneg_of_mem_Icc hmem
  43  have hcot : 0 ≤ Real.cot ϑ := by
  44    -- Rewrite `cot` as `cos / sin` on reals.
  45    simpa [Real.cot_eq_cos_div_sin] using (div_nonneg hcos hsin)
  46  have hprod : 0 ≤ 2 * Real.cot ϑ := by
  47    have htwo : 0 ≤ (2 : ℝ) := by norm_num
  48    exact mul_nonneg htwo hcot
  49  simpa using add_le_add_left hprod 1
  50
  51/-- Recognition profile is positive -/
  52lemma recognitionProfile_pos (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  53  0 < recognitionProfile ϑ := by
  54  have hy : 1 ≤ 1 + 2 * Real.cot ϑ := arcosh_arg_ge_one ϑ hϑ
  55  have hypos : 0 < 1 + 2 * Real.cot ϑ := lt_of_lt_of_le zero_lt_one hy
  56  have hs : 0 ≤ Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1) := Real.sqrt_nonneg _
  57  exact add_pos_of_pos_of_nonneg hypos hs