def
definition
genuineRegularFactorPhaseAt
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 486.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
radius -
of -
phase -
identity -
is -
of -
is -
of -
is -
of -
is -
RegularFactorPhase -
QuantitativeLocalFactorization -
regularFactorPhaseFromWitness -
that -
phase -
constant -
identity
used by
formal source
483/-! ### §5b. Perturbation witness for genuine phase family -/
484
485/-- Extract the regular factor phase at level `n` from the genuine family. -/
486noncomputable def genuineRegularFactorPhaseAt
487 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
488 RegularFactorPhase :=
489 let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
490 let hd : (0 : ℝ) < ↑n + 1 := by linarith
491 let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
492 regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
493 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
494 qlf.logDerivBound qlf.logDerivBound_pos
495
496/-- The log-derivative bound of the genuine regular factor phase at level `n`
497is definitionally `qlf.logDerivBound * (qlf.radius / (n + 1))`.
498
499This is the critical identity that connects the analytic input
500(`QuantitativeLocalFactorization.logDerivBound`) to the phase-level
501Lipschitz constant, enabling discharge of perturbation-witness bounds. -/
502theorem genuineRegularFactorPhaseAt_logDerivBound
503 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
504 (genuineRegularFactorPhaseAt qlf n hn).logDerivBound =
505 qlf.logDerivBound * (qlf.radius / (↑n + 1)) := by
506 rfl
507
508/-- Absolute bound on epsilon at level `n`: the perturbation increment
509is bounded by `M * R * 2π / (8n(n+1))`. -/
510theorem epsilon_abs_bound
511 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
512 |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| ≤
513 qlf.logDerivBound * (qlf.radius / (↑n + 1)) * (2 * π / (8 * ↑n)) := by
514 exact (genuineRegularFactorPhaseAt qlf n hn).increment_bound n hn j
515
516/-- At the genuine phase family, `|ε| ≤ M * R / (n+1) * π / (4n)`, and