{
  "file_path": "D:\\Python\\Quantum\\NGUYEN.md",
  "offset": 148,
  "limit": 22
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean",
    "content": "    have hC : Real.log (Real.log T) \u2264 Real.log (Real.log (Real.sqrt (n : \u211d) + 1)) := by\n      apply Real.log_le_log (by linarith [hlog1] : (0 : \u211d) < Real.log T)\n      have h1 : (1 : \u211d) \u2264 Real.log (Real.sqrt (n : \u211d) + 1) := by\n        have ht2 : (0 : \u211d) < Real.sqrt (n : \u211d) + 1 := by positivity\n        rw [Real.le_log_iff_exp_le ht2]\n        have he := Real.exp_one_lt_d9.le\n        nlinarith [hsqrt316, he]\n      have h2 : Real.log T \u2264 Real.log (Real.sqrt (n : \u211d) + 1) := hB\n      linarith [h2, hlog1]\n    have hconst : (0 : \u211d) \u2264 1 / (2 * Real.pi) := by positivity\n    have hA' := mul_le_mul_of_nonneg_left hA hconst\n    nlinarith [hA', hB, hC]\n  have hX : 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) \u2264\n      4 * (Real.sqrt (n : \u211d) + 1) *\n        ((2 / 3) * Z2hat (Real.sqrt (n : \u211d) + 1) + 10.5 * Real.log (Real.sqrt (n : \u211d) + 1 + 2) + 48) := by\n    have hZ := Z2hat_mono hT1 hTn1\n    have hlog := Real.log_le_log (by linarith : (0 : \u211d) < T + 2)\n      (by linarith [hTn1] : T + 2 \u2264 Real.sqrt (n : \u211d) + 1 + 2)\n    have hXle : (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 \u2264\n        (2 / 3) * Z2hat (Real.sqrt (n : \u211d) + 1) + 10.5 * Real.log (Real.sqrt (n : \u211d) + 1 + 2) + 48 := by\n      nlinarith [hZ, hlog]\n    have hX0' : (0 : \u211d) \u2264 (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 := by\n      have h1 := Z2hat_nonneg hT1\n      nlinarith [hlogT1]",
    "numLines": 24,
    "startLine": 1606,
    "totalLines": 1706
  }
}