[{"type":"thinking","thinking":"- `ContinuousOn.intervalIntegrable (hu : ContinuousOn u (uIcc a b)) : IntervalIntegrable u μ a b` ✓ (takes uIcc, no hab needed).\n- `Jlag_differentiableAt {n} {s} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) : DifferentiableAt ℂ (Jlag n) s` ✓ (LiSides:82).\n- `riemannZeta_conj (s : ℂ) : riemannZeta (conj s) = conj (riemannZeta s)` ✓.\n\nNow — for the +T full-side proof, plan:\n\n```lean\n/-- **6-c-v (horizontal assembly)**: the full horizontal side split at 3 —\nmid bound (6-c-iv) + the DL-5 dog-leg tail. -/\ntheorem hIntegral_Jlag_full_norm_le (hZC) (hZC2) (hNLZ) {n} (hn : 100000 ≤ n) {T}\n    (hTwide) (hTn) (hTn1) :\n    ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) T‖ ≤\n      (Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (√n+2)) +\n        (3 - -5/2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ) := by\n  have hnR : ... ; have h10T : ... ; have hT0 : 0 < T := ...\n  have hn16 : 16 ≤ n := by omega\n  have hn1 : 1 ≤ n := by omega\n  have h3le : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by ... (√n ≥ 316)\n  -- split at 3\n  have hsplit : HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) T =\n      HIntegral (Jlag n) (-5/2) 3 T + HIntegral (Jlag n) 3 (2 * Real.sqrt n) T :=\n    HIntegral_split hInt1 hInt2\n  rw [hsplit]\n  calc ‖HIntegral (Jlag n) (-5/2) 3 T + HIntegral (Jlag n) 3 (2 * Real.sqrt n) T‖\n      ≤ ‖HIntegral (Jlag n) (-5/2) 3 T‖ + ‖HIntegral (Jlag n) 3 (2 * Real.sqrt n) T‖ :=\n        norm_add_le _ _\n    _ ≤ (mid bound) + DogLegRight (n : ℝ) := by\n        have hmid := hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n        have htail := hIntegral_Jlag_low_le_dogLegUpper hn16 hTn hTn1\n        -- htail : ‖HIntegral (Jlag n) 3 (2√n) T‖ ≤ ((√n+1)/2)(e^{5/2}+1)/2 + 8.38 + IIMaj/4\n        -- DogLegRight n = exactly that\n        rw [show DogLegRight (n : ℝ) = ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +\n          (8.38 : ℝ) + IIMaj (n : ℝ) / 4 from rfl]\n        linarith [hmid, htail]\n```\n\nDogLegRight (n:ℝ) — its def: ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj n/4 — and htail's RHS: `((Real.sqrt (n: ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n: ℝ) / 4` — DogLegRight unfolds to EXACTLY that (modulo the 8.38 being bare vs (8.38 : ℝ) — same ✓). So `DogLegRight (n:ℝ) = ...` by rfl ✓ (defeq — the show-rfl should work; or `unfold DogLegRight`).\n\nHmm — htail (DL-5) needs (hn : 16 ≤ n) — hn16 := by omega ✓.\n\nhInt1 : IntervalIntegrable (fun σ => Jlag n (↑σ+↑T·I)) volume (−5/2) 3 — via the +T-path continuity (zeta_ne_zero_horizontal — global):\n```lean\n  have hJcontP : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n    intro σ\n    have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by\n      intro h\n      have him := congrArg Complex.im h\n      simp at him\n      linarith [hT0]\n    have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n    have hB := continuousAt_logDeriv_zeta hs1 (zeta_ne_zero_horizontal hTwide hn1 hTn hTn1)\n    show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n    exact hA.mul hB.neg\n  have hcontJP : Continuous fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n    rw [continuous_iff_continuousAt]\n    intro σ\n    have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=\n      hpath.continuousAt\n    exact ContinuousAt.comp (g := Jlag n) (f := ...) (x := σ) (hJcontP σ) hf\n  have hInt1 : IntervalIntegrable (fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I))\n      MeasureTheory.volume (-5/2) 3 := hcontJP.intervalIntegrable _ _\n```\n\nhInt2 : IntervalIntegrable ... 3 (2√n) — via the dog-leg differentiability (ContinuousOn on uIcc(3, 2√n)):\n```lean\n  have hInt2 : IntervalIntegrable (fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I))\n      MeasureTheory.volume 3 (2 * Real.sqrt (n : ℝ)) := by\n    apply ContinuousOn.intervalIntegrable\n    rw [Set.uIcc_of_le h3le]\n    intro σ hσ\n    obtain ⟨hσ1, hσ2⟩ := hσ  -- 3 ≤ σ ≤ 2√n\n    have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp\n    have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp\n    exact (Jlag_differentiableAt_dogleg (n := n) (s := ((σ : ℝ) + (T : ℝ) * Complex.I))\n      (by rw [hre]; exact hσ1) (by rw [him]; exact hT0)).continuousAt.continuousWithinAt\n```\n\nHmm — ContinuousOn f s := ∀ x ∈ s, ContinuousWithinAt f s x — so intro σ hσ; exact ....continuousWithinAt ✓ — wait — ContinuousOn f s is DEFINED as ∀ x ∈ s, ContinuousWithinAt f s x ✓. So `intro σ hσ` then produce ContinuousWithinAt — from DifferentiableAt.continuousAt.continuousWithinAt ✓.\n\nh3le : 3 ≤ 2√n — from √n ≥ 316 (h10T-chain): 2√n ≥ 632 ≥ 3 ✓:\n```lean\n  have h3le : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by\n    have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n      rw [Real.le_sqrt (by norm_num) (by positivity)]\n      nlinarith [hnR]\n    nlinarith [h1]\n```\n\nAnd `Set.uIcc_of_le h3le : uIcc 3 (2√n) = Icc 3 (2√n)` — `Set.uIcc_of_le (hab : a ≤ b) : uIcc a b = Icc a b` ✓ (used in DL-1's holomorphicOn proof: Set.uIcc_of_le hTU ✓).\n\nThen the full theorem assembly. And hT0 : 0 < T := by (from √n > 0): Real.sqrt_pos.mpr (by linarith [hnR]) then linarith.\n\nFor the −T full theorem: conj at the FULL level:\n```lean\ntheorem hIntegral_Jlag_full_neg_norm_le (same hyps) :\n    ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) (-T)‖ ≤ (same RHS) := by\n  have hT0 : (0:ℝ) < T := ...\n  have hconj : HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) (-T) =\n      (starRingEnd ℂ) (HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) T) := by\n    unfold HIntegral\n    rw [← intervalIntegral.intervalIntegral_conj]\n    apply intervalIntegral.integral_congr\n    intro σ hσ\n    show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n      (starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))\n    have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n        (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by simp\n    rw [hid2]\n    exact Jlag_conj n (by\n      intro h\n      have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp\n      rw [h] at him\n      simp at him\n      linarith [hT0])\n  rw [hconj, Complex.norm_conj]\n  exact hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n```\n— verbatim DL-5/6-c-iv-neg pattern ✓.\n\nThen the two-sides:\n```lean\ntheorem hIntegral_Jlag_full_two_sides (hZC) (hZC2) (hNLZ) {n} (hn : 100000 ≤ n) {T}\n    (hTwide) (hTn) (hTn1) :\n    ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) T‖ +\n      ‖HIntegral (Jlag n) (-5/2) (2 * Real.sqrt n) (-T)‖ ≤\n      2 * ((Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (√n+2)) +\n          (3 - -5/2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) := by\n  rw [show (2 : ℝ) * (X + DogLegRight (n:ℝ)) = (X + DogLegRight (n:ℝ)) + (X + DogLegRight (n:ℝ)) by ring]\n  exact add_le_add (hIntegral_Jlag_full_norm_le ...) (hIntegral_Jlag_full_neg_norm_le ...)\n```\n(clone dogLegUpper_two_sides's structure ✓.)\n\nHmm — wait — the fold's horizontal charge: \"2(e⁴+1)(NI + 5.5(...)) + 2·DogLegRight\" — my two-sides gives 2·(midBound + DogLegRight) = 2·midBound + 2·DogLegRight ✓ same thing (midBound = (e⁴+1)(NI + 5.5(...))). ✓\n\nNow — do I also need the per-side FULL bounds (not just two-sides)? The 6-d fold uses the SUM via the rectangle decomposition — the two-sides lemma suffices. But having the single-side theorems is natural anyway (the neg one needs the pos one). OK.\n\nOne more check — `HIntegral_split` (from §1): (h1 : IntervalIntegrable (fun σ => f (↑σ + ↑y·I)) volume a b) (h2 : ... b c) : HIntegral f a c y = HIntegral f a b y + HIntegral f b c y ✓ — my hInt1 (a=-5/2, b=3), hInt2 (b=3, c=2√n) ✓.\n\nAlso — `intervalIntegral.integral_const_mul` — hmm not needed here.\n\nAlso — the htail's exact RHS — from DL-5 (line 1302-1304): `((Real.sqrt (n: ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n: ℝ) / 4` ✓ — and DogLegRight (n : ℝ) := `((Real.sqrt n + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + 8.38 + IIMaj n / 4` — the show-rfl: `show DogLegRight (n : ℝ) = ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n : ℝ) / 4 from rfl` — defeq ✓ (the def unfolds; 8.38 vs (8.38 : ℝ) — same term ✓; `Real.sqrt n` vs `Real.sqrt (n : ℝ)` — in the def, DogLegRight's param is named n : ℝ — applied at (n:ℝ) = ↑n — Real.sqrt ↑n ✓ same ✓). So `from rfl` ✓. If rfl fails, `from by unfold DogLegRight`.\n\nLet me write §5 now. Also mark the header §5 and the file-top comment.","signature":""},{"type":"text","text":"All signatures confirmed. Writing §5 (6-c-v) — the horizontal assembly."},{"type":"tool_use","id":"Edit_147","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean","old_string":"  rw [hconj, Complex.norm_conj]\n  exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\nend NguyenRH1","new_string":"  rw [hconj, Complex.norm_conj]\n  exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\n/-! ## 5. 6-c-v: the full horizontal assembly (mid + DL-5 tails) -/\n\n/-- **6-c-v (the +T full horizontal side)**: split at 3 — the 6-c-iv mid\nbound + the DL-5 dog-leg tail charge. -/\ntheorem hIntegral_Jlag_full_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n    (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n    (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\n      ρ.im < Real.sqrt (n : ℝ) + 2 →\n        1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\n    (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n    ‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T‖ ≤\n      (Real.exp 4 + 1) *\n        (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n          (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ) := by\n  classical\n  have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n  have h10T : (10 : ℝ) ≤ T := by\n    have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n      rw [Real.le_sqrt (by norm_num) (by positivity)]\n      nlinarith [hnR]\n    linarith\n  have hT0 : (0 : ℝ) < T := by linarith\n  have hn1 : 1 ≤ n := by omega\n  have hn16 : 16 ≤ n := by omega\n  have h3le : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by\n    have h1 : (10 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n      rw [Real.le_sqrt (by norm_num) (by positivity)]\n      nlinarith [hnR]\n    nlinarith [h1]\n  -- the mid-path continuity (zero-free via the wide pigeonhole)\n  have hJcontP : ∀ σ : ℝ, ContinuousAt (Jlag n) ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n    intro σ\n    have hs1 : ((σ : ℝ) + (T : ℝ) * Complex.I) ≠ 1 := by\n      intro h\n      have him := congrArg Complex.im h\n      simp at him\n      linarith [hT0]\n    have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n    have hB := continuousAt_logDeriv_zeta hs1 (zeta_ne_zero_horizontal hTwide hn1 hTn hTn1)\n    show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n    exact hA.mul hB.neg\n  have hpath : Continuous fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I) := by\n    fun_prop\n  have hcontJP : Continuous fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I) := by\n    rw [continuous_iff_continuousAt]\n    intro σ\n    have hf : ContinuousAt (fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) σ :=\n      hpath.continuousAt\n    exact ContinuousAt.comp (g := Jlag n)\n      (f := fun u : ℝ => ((u : ℝ) + (T : ℝ) * Complex.I)) (x := σ) (hJcontP σ) hf\n  have hInt1 : IntervalIntegrable (fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I))\n      MeasureTheory.volume (-5 / 2) 3 := hcontJP.intervalIntegrable _ _\n  -- the tail-path continuity (zero-free by re ≥ 3 > 1, DL-1)\n  have hInt2 : IntervalIntegrable (fun σ : ℝ => Jlag n ((σ : ℝ) + (T : ℝ) * Complex.I))\n      MeasureTheory.volume 3 (2 * Real.sqrt (n : ℝ)) := by\n    apply ContinuousOn.intervalIntegrable\n    rw [Set.uIcc_of_le h3le]\n    intro σ hσ\n    obtain ⟨hσ1, hσ2⟩ := hσ\n    have hre : ((σ : ℝ) + (T : ℝ) * Complex.I).re = σ := by simp\n    have him : ((σ : ℝ) + (T : ℝ) * Complex.I).im = T := by simp\n    exact (Jlag_differentiableAt_dogleg (s := ((σ : ℝ) + (T : ℝ) * Complex.I))\n      (by rw [hre]; exact hσ1) (by rw [him]; exact hT0)).continuousAt.continuousWithinAt\n  -- split at 3 and assemble\n  have hsplit : HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T =\n      HIntegral (Jlag n) (-5 / 2) 3 T + HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T :=\n    HIntegral_split hInt1 hInt2\n  have hmid := hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n  have htail := hIntegral_Jlag_low_le_dogLegUpper hn16 hTn hTn1\n  have hDLR : DogLegRight (n : ℝ) = ((Real.sqrt (n : ℝ) + 1) / 2) *\n      (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) + IIMaj (n : ℝ) / 4 := rfl\n  rw [hsplit, hDLR]\n  calc ‖HIntegral (Jlag n) (-5 / 2) 3 T +\n        HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖\n      ≤ ‖HIntegral (Jlag n) (-5 / 2) 3 T‖ +\n        ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ := norm_add_le _ _\n    _ ≤ (Real.exp 4 + 1) *\n          (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n            (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) +\n          (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n            IIMaj (n : ℝ) / 4) :=\n        add_le_add hmid htail\n\n/-- **6-c-v (the −T full horizontal side)**: the conj trick at the full\nlevel (no split needed — intervalIntegral_conj is unconditional). -/\ntheorem hIntegral_Jlag_full_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n    (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n    (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\n      ρ.im < Real.sqrt (n : ℝ) + 2 →\n        1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\n    (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n    ‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤\n      (Real.exp 4 + 1) *\n        (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n          (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ) := by\n  have hnR : (100000 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n  have hT0 : (0 : ℝ) < T := by\n    have h1 : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)\n    linarith\n  have hconj : HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T) =\n      (starRingEnd ℂ) (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T) := by\n    unfold HIntegral\n    rw [← intervalIntegral.intervalIntegral_conj]\n    apply intervalIntegral.integral_congr\n    intro σ hσ\n    show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n      (starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))\n    have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =\n        (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by simp\n    rw [hid2]\n    exact Jlag_conj n (by\n      intro h\n      have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp\n      rw [h] at him\n      simp at him\n      linarith [hT0])\n  rw [hconj, Complex.norm_conj]\n  exact hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\n/-- **6-c-v (the two horizontal sides)**: the horizontal assembly charge —\n2·(mid bound) + 2·DogLegRight. -/\ntheorem hIntegral_Jlag_full_two_sides (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n    (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n    (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt (n : ℝ) - 1 < ρ.im →\n      ρ.im < Real.sqrt (n : ℝ) + 2 →\n        1 / (9 * C0hat (Real.sqrt (n : ℝ) + 2)) ≤ |ρ.im - T|)\n    (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n    ‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) T‖ +\n      ‖HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤\n      2 * ((Real.exp 4 + 1) *\n        (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n          (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) := by\n  rw [show (2 : ℝ) * ((Real.exp 4 + 1) *\n        (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n          (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) =\n      ((Real.exp 4 + 1) *\n        (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n          (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) +\n      ((Real.exp 4 + 1) *\n        (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : ℝ) + 2)) +\n          (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : ℝ)) by ring]\n  exact add_le_add (hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1)\n    (hIntegral_Jlag_full_neg_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1)\n\nend NguyenRH1"},"extra_content":null}]