def
definition
def or abbrev
genuineZetaDerivedPhaseData
show as:
view Lean formalization →
formal statement (Lean)
420private noncomputable def genuineZetaDerivedPhaseData
421 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
422 ContinuousPhaseData :=
proof body
Definition body.
423 let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
424 let hd : (0 : ℝ) < ↑n + 1 := by linarith
425 let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
426 let hr : 0 < qlf.radius / (↑n + 1) := div_pos qlf.radius_pos hd
427 let hrw : qlf.radius / (↑n + 1) < qlf.radius :=
428 div_lt_self qlf.radius_pos hgt1
429 let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
430 (qlf.radius / (↑n + 1)) hr hrw qlf.logDerivBound qlf.logDerivBound_pos
431 { center := qlf.center
432 radius := qlf.radius / (↑n + 1)
433 radius_pos := hr
434 phase := fun θ => (qlf.order : ℝ) * θ + rfp.phase θ
435 phase_continuous := by
436 exact (continuous_const.mul continuous_id).add rfp.phase_continuous
437 charge := -qlf.order
438 phase_winding := by
439 simp only [add_sub_add_comm]
440 have hw_pole : (qlf.order : ℝ) * (2 * π) - (qlf.order : ℝ) * 0 =
441 -(2 * π * ((-qlf.order : ℤ) : ℝ)) := by
442 simp [Int.cast_neg]; ring
443 have hw_reg := rfp.toContinuousPhaseData.phase_winding
444 rw [rfp.charge_zero] at hw_reg
445 simp at hw_reg
446 rw [hw_pole, hw_reg, add_zero] }
447
448/-- The genuine phase data has the correct charge. -/