11.20. HardyZeta.ThetaPath🔗

def thetaCuspPath (u : ℝ) : ℂ := I * (exp (-2 * (u : ℂ) * I) - 1) @[simp] theorem thetaCuspPath_zero : thetaCuspPath 0 = 0 := by⊢ thetaCuspPath 0 = 0 simp [thetaCuspPath]All goals completed! 🐙theorem thetaCuspPath_eq (u : ℝ) : thetaCuspPath u = exp (2 * I * ((Real.pi / 4 - u : ℝ) : ℂ)) - I := byu:ℝ⊢ thetaCuspPath u = cexp (2 * I * ↑(Real.pi / 4 - u)) - I have he : 2 * I * ((Real.pi / 4 - u : ℝ) : ℂ) = (Real.pi : ℂ) / 2 * I + (-2 * (u : ℂ) * I) := by push_castu:ℝ⊢ 2 * I * (↑Real.pi / 4 - ↑u) = ↑Real.pi / 2 * I + -2 * ↑u * I; ringu:ℝhe:2 * I * ↑(Real.pi / 4 - u) = ↑Real.pi / 2 * I + -2 * ↑u * I⊢ thetaCuspPath u = cexp (2 * I * ↑(Real.pi / 4 - u)) - I rw [he,u:ℝhe:2 * I * ↑(Real.pi / 4 - u) = ↑Real.pi / 2 * I + -2 * ↑u * I⊢ thetaCuspPath u = cexp (↑Real.pi / 2 * I + -2 * ↑u * I) - I exp_add,u:ℝhe:2 * I * ↑(Real.pi / 4 - u) = ↑Real.pi / 2 * I + -2 * ↑u * I⊢ thetaCuspPath u = cexp (↑Real.pi / 2 * I) * cexp (-2 * ↑u * I) - I exp_pi_div_two_mul_Iu:ℝhe:2 * I * ↑(Real.pi / 4 - u) = ↑Real.pi / 2 * I + -2 * ↑u * I⊢ thetaCuspPath u = I * cexp (-2 * ↑u * I) - I]u:ℝhe:2 * I * ↑(Real.pi / 4 - u) = ↑Real.pi / 2 * I + -2 * ↑u * I⊢ thetaCuspPath u = I * cexp (-2 * ↑u * I) - I unfold thetaCuspPathu:ℝhe:2 * I * ↑(Real.pi / 4 - u) = ↑Real.pi / 2 * I + -2 * ↑u * I⊢ I * (cexp (-2 * ↑u * I) - 1) = I * cexp (-2 * ↑u * I) - I ringAll goals completed! 🐙theorem hasDerivAt_thetaCuspPath_zero : HasDerivAt thetaCuspPath (2 : ℂ) 0 := by⊢ HasDerivAt thetaCuspPath 2 0 have h0 := ((hasDerivAt_id (0 : ℝ)).ofReal_comp.const_mul (-2 : ℂ)).mul_const Ih0:HasDerivAt (fun y => -2 * ↑(id y) * I) (-2 * ↑1 * I) 0⊢ HasDerivAt thetaCuspPath 2 0 have h := (h0.cexp.sub_const 1).const_mul Ih0:HasDerivAt (fun y => -2 * ↑(id y) * I) (-2 * ↑1 * I) 0h:HasDerivAt (fun y => I * (cexp (-2 * ↑(id y) * I) - 1)) (I * (cexp (-2 * ↑(id 0) * I) * (-2 * ↑1 * I))) 0⊢ HasDerivAt thetaCuspPath 2 0 have h' : HasDerivAt thetaCuspPath (I * (exp (-2 * (0 : ℂ) * I) * (-2 * (1 : ℂ) * I))) (0 : ℝ) := hh0:HasDerivAt (fun y => -2 * ↑(id y) * I) (-2 * ↑1 * I) 0h:HasDerivAt (fun y => I * (cexp (-2 * ↑(id y) * I) - 1)) (I * (cexp (-2 * ↑(id 0) * I) * (-2 * ↑1 * I))) 0h':HasDerivAt thetaCuspPath (I * (cexp (-2 * 0 * I) * (-2 * 1 * I))) 0⊢ HasDerivAt thetaCuspPath 2 0 norm_num [mul_left_comm I 2 I] at h'h0:HasDerivAt (fun y => -2 * ↑(id y) * I) (-2 * ↑1 * I) 0h:HasDerivAt (fun y => I * (cexp (-2 * ↑(id y) * I) - 1)) (I * (cexp (-2 * ↑(id 0) * I) * (-2 * ↑1 * I))) 0h':HasDerivAt thetaCuspPath 2 0⊢ HasDerivAt thetaCuspPath 2 0 exact h'All goals completed! 🐙theorem tendsto_thetaCuspPath_div : Tendsto (fun u : ℝ ↦ thetaCuspPath u / (u : ℂ)) (𝓝[>] 0) (𝓝 2) := by⊢ Tendsto (fun u => thetaCuspPath u / ↑u) (𝓝[>] 0) (𝓝 2) simpa [thetaCuspPath_zero, real_smul, div_eq_mul_inv, mul_comm] using hasDerivAt_thetaCuspPath_zero.tendsto_slope_zero_rightAll goals completed! 🐙theorem tendsto_thetaCuspPath : Tendsto thetaCuspPath (𝓝[>] 0) (𝓝 0) := by⊢ Tendsto thetaCuspPath (𝓝[>] 0) (𝓝 0) simpa using hasDerivAt_thetaCuspPath_zero.continuousAt.tendsto.mono_left nhdsWithin_le_nhdsAll goals completed! 🐙 /-- The approach stays inside one closed sector and never hits the cusp. -/theorem eventually_thetaCuspPath_sector : ∀ᶠ u : ℝ in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ (1 / 3 : ℝ) * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re := by⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hr : Tendsto (fun u : ℝ ↦ (thetaCuspPath u / (u : ℂ)).re) (𝓝[>] 0) (𝓝 (2 : ℝ)) := by simpa only [Function.comp_def, show (2 : ℂ).re = (2 : ℝ) from rfl] using (continuous_re.tendsto (2 : ℂ)).comp tendsto_thetaCuspPath_divhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hn : Tendsto (fun u : ℝ ↦ ‖thetaCuspPath u / (u : ℂ)‖) (𝓝[>] 0) (𝓝 (2 : ℝ)) := by simpa using tendsto_thetaCuspPath_div.normhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hr' := hr.eventually (lt_mem_nhds (byhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)⊢ 1 < 2 norm_numAll goals completed! 🐙 : (1 : ℝ) < 2))hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).re⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hn' := hn.eventually (gt_mem_nhds (byhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).re⊢ 2 < 3 norm_numAll goals completed! 🐙 : (2 : ℝ) < 3))hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re filter_upwards [hr', hn', self_mem_nhdsWithin] with u hurhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).re⊢ ‖thetaCuspPath u / ↑u‖ < 3 → u ∈ Set.Ioi 0 → thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re hunhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3⊢ u ∈ Set.Ioi 0 → thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re huhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hu0 : 0 < u := huhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hreq : (thetaCuspPath u / (u : ℂ)).re = (thetaCuspPath u).re / u := by⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re simp [div_re]hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < u⊢ (thetaCuspPath u).re * u / (u * u) = (thetaCuspPath u).re / u field_simphr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hneq : ‖thetaCuspPath u / (u : ℂ)‖ = ‖thetaCuspPath u‖ / u := by⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re rw [norm_div,hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / u⊢ ‖thetaCuspPath u‖ / ‖↑u‖ = ‖thetaCuspPath u‖ / u norm_real,hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / u⊢ ‖thetaCuspPath u‖ / ‖u‖ = ‖thetaCuspPath u‖ / u Real.norm_eq_abs,hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / u⊢ ‖thetaCuspPath u‖ / |u| = ‖thetaCuspPath u‖ / u abs_of_pos hu0hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / u⊢ ‖thetaCuspPath u‖ / u = ‖thetaCuspPath u‖ / u]hr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u / ↑u).rehun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re rw [hreqhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re] at hurhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u / ↑u‖ < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re rw [hneqhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re] at hunhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hre : u < (thetaCuspPath u).re := by⊢ ∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re simpa using (lt_div_iff₀ hu0).mp hurhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).re⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re have hnorm : ‖thetaCuspPath u‖ < 3 * u := (div_lt_iff₀ hu0).mp hunhr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).rehnorm:‖thetaCuspPath u‖ < 3 * u⊢ thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re constructorlefthr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).rehnorm:‖thetaCuspPath u‖ < 3 * u⊢ thetaCuspPath u ≠ 0righthr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).rehnorm:‖thetaCuspPath u‖ < 3 * u⊢ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re ·lefthr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).rehnorm:‖thetaCuspPath u‖ < 3 * u⊢ thetaCuspPath u ≠ 0 intro helefthr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).rehnorm:‖thetaCuspPath u‖ < 3 * uhe:thetaCuspPath u = 0⊢ False simp [he] at hrelefthr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhnorm:‖thetaCuspPath u‖ < 3 * uhe:thetaCuspPath u = 0hre:u < 0⊢ False linarithAll goals completed! 🐙 ·righthr:Tendsto (fun u => (thetaCuspPath u / ↑u).re) (𝓝[>] 0) (𝓝 2)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖) (𝓝[>] 0) (𝓝 2)hr':∀ᶠ (x : ℝ) in 𝓝[>] 0, 1 < (thetaCuspPath x / ↑x).rehn':∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖thetaCuspPath x / ↑x‖ < 3u:ℝhur:1 < (thetaCuspPath u).re / uhun:‖thetaCuspPath u‖ / u < 3hu:u ∈ Set.Ioi 0hu0:0 < uhreq:(thetaCuspPath u / ↑u).re = (thetaCuspPath u).re / uhneq:‖thetaCuspPath u / ↑u‖ = ‖thetaCuspPath u‖ / uhre:u < (thetaCuspPath u).rehnorm:‖thetaCuspPath u‖ < 3 * u⊢ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re linarithAll goals completed! 🐙 /-- Every inverse natural power of the path parameter is absorbed by cusp decay. -/theorem tendsto_thetaCuspPath_weighted (n : ℕ) : Tendsto (fun u : ℝ ↦ u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) := byn:ℕ⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) have hs := eventually_thetaCuspPath_sectorn:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) have hd := tendsto_weighted_psi_cusp (byn:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re⊢ 0 < 1 / 3 norm_numAll goals completed! 🐙 : (0 : ℝ) < 1 / 3) (n : ℝ) tendsto_thetaCuspPath (hs.mono fun _ h ↦ h.1) (hs.mono fun _ h ↦ h.2)n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) have hn : Tendsto (fun u : ℝ ↦ ‖thetaCuspPath u / (u : ℂ)‖ ^ n) (𝓝[>] 0) (𝓝 ((2 : ℝ) ^ n)) := by simpa using tendsto_thetaCuspPath_div.norm.pow nn:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) have hl := hn.mul hdn:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 (2 ^ n * 0))⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) simp only [mul_zero, Real.rpow_natCast] at hln:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) apply hl.congr'n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)⊢ (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) =ᶠ[𝓝[>] 0] fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ filter_upwards [hs, self_mem_nhdsWithin] with u hn:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).re⊢ u ∈ Set.Ioi 0 → ‖thetaCuspPath u / ↑u‖ ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ hun:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0⊢ ‖thetaCuspPath u / ↑u‖ ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ have hu0 : 0 < u := hun:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < u⊢ ‖thetaCuspPath u / ↑u‖ ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ have hz : ‖thetaCuspPath u‖ ≠ 0 := norm_ne_zero_iff.mpr h.1n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ ‖thetaCuspPath u / ↑u‖ ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ rw [norm_div,n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / ‖↑u‖) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ norm_real,n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / ‖u‖) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ Real.norm_eq_abs,n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / |u|) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ abs_of_pos hu0n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / u) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖]n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / u) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ have he : (‖thetaCuspPath u‖ / u) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n) = u⁻¹ ^ n := byn:ℕ⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) (𝓝[>] 0) (𝓝 0) rw [← mul_pown:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / u * ‖thetaCuspPath u‖⁻¹) ^ n = u⁻¹ ^ n]n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ (‖thetaCuspPath u‖ / u * ‖thetaCuspPath u‖⁻¹) ^ n = u⁻¹ ^ n congr 1e_an:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0⊢ ‖thetaCuspPath u‖ / u * ‖thetaCuspPath u‖⁻¹ = u⁻¹ field_simpn:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0he:(‖thetaCuspPath u‖ / u) ^ n * ‖thetaCuspPath u‖⁻¹ ^ n = u⁻¹ ^ n⊢ (‖thetaCuspPath u‖ / u) ^ n * (‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖) = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ rw [← mul_assoc,n:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0he:(‖thetaCuspPath u‖ / u) ^ n * ‖thetaCuspPath u‖⁻¹ ^ n = u⁻¹ ^ n⊢ (‖thetaCuspPath u‖ / u) ^ n * ‖thetaCuspPath u‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ hen:ℕhs:∀ᶠ (u : ℝ) in 𝓝[>] 0, thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehd:Tendsto (fun t => ‖thetaCuspPath t‖⁻¹ ^ ↑n * ‖1 / 2 + psi (I + thetaCuspPath t)‖) (𝓝[>] 0) (𝓝 0)hn:Tendsto (fun u => ‖thetaCuspPath u / ↑u‖ ^ n) (𝓝[>] 0) (𝓝 (2 ^ n))hl:Tendsto (fun x => ‖thetaCuspPath x / ↑x‖ ^ n * (‖thetaCuspPath x‖⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath x)‖)) (𝓝[>] 0) (𝓝 0)u:ℝh:thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖thetaCuspPath u‖ ≤ (thetaCuspPath u).rehu:u ∈ Set.Ioi 0hu0:0 < uhz:‖thetaCuspPath u‖ ≠ 0he:(‖thetaCuspPath u‖ / u) ^ n * ‖thetaCuspPath u‖⁻¹ ^ n = u⁻¹ ^ n⊢ u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖ = u⁻¹ ^ n * ‖1 / 2 + psi (I + thetaCuspPath u)‖]All goals completed! 🐙 /-- The exact exponential argument in the proposed transform formula has flat cusp values. -/theorem tendsto_theta_argument_weighted (n : ℕ) : Tendsto (fun u : ℝ ↦ u⁻¹ ^ n * ‖1 / 2 + psi (exp (2 * I * ((Real.pi / 4 - u : ℝ) : ℂ)))‖) (𝓝[>] 0) (𝓝 0) := byn:ℕ⊢ Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + psi (cexp (2 * I * ↑(Real.pi / 4 - u)))‖) (𝓝[>] 0) (𝓝 0) simpa only [thetaCuspPath_eq, add_sub_cancel] using tendsto_thetaCuspPath_weighted nAll goals completed! 🐙 /-- The theta remainder in Hardy's proposed open-strip transform identity. -/def thetaBoundaryRemainder (α : ℝ) : ℂ := exp (I * (α : ℂ) / 2) * (1 / 2 + psi (exp (2 * I * (α : ℂ))))theorem norm_thetaBoundaryRemainder (α : ℝ) : ‖thetaBoundaryRemainder α‖ = ‖1 / 2 + psi (exp (2 * I * (α : ℂ)))‖ := byα:ℝ⊢ ‖thetaBoundaryRemainder α‖ = ‖1 / 2 + psi (cexp (2 * I * ↑α))‖ simp [thetaBoundaryRemainder, norm_exp, mul_re]All goals completed! 🐙theorem tendsto_thetaBoundaryRemainder_weighted (n : ℕ) : Tendsto (fun u : ℝ ↦ u⁻¹ ^ n * ‖thetaBoundaryRemainder (Real.pi / 4 - u)‖) (𝓝[>] 0) (𝓝 0) := byn:ℕ⊢ Tendsto (fun u => u⁻¹ ^ n * ‖thetaBoundaryRemainder (Real.pi / 4 - u)‖) (𝓝[>] 0) (𝓝 0) simpa only [norm_thetaBoundaryRemainder] using tendsto_theta_argument_weighted nAll goals completed! 🐙