def
definition
def or abbrev
genuineZetaDerivedPhasePerturbationWitness
show as:
view Lean formalization →
formal statement (Lean)
735noncomputable def genuineZetaDerivedPhasePerturbationWitness
736 (sensor : DefectSensor)
737 (qlf : QuantitativeLocalFactorization)
738 (horder : qlf.order = -sensor.charge) :
739 DefectPhasePerturbationWitness (genuineZetaDerivedPhaseFamily sensor qlf horder) where
740 epsilon := fun n hn j =>
proof body
Definition body.
741 (genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j
742 increment_eq := by
743 intro n hn j
744 simp only [genuineZetaDerivedPhaseFamily, genuineZetaDerivedPhaseData,
745 ContinuousPhaseData.sampleIncrements, defectPhasePureIncrement, horder]
746 simp only [genuineRegularFactorPhaseAt, regularFactorPhaseFromWitness, mkRegularFactorPhase]
747 congr 1
748 push_cast
749 ring
750 small := epsilon_log_phi_small qlf
751 linear_term_bounded := by
752 refine ⟨qlf.logDerivBound * qlf.radius * (2 * π) *
753 (Real.log Constants.phi * Real.sinh (Real.log Constants.phi *
754 (π * |(-sensor.charge : ℤ)| / 4))), ?_⟩
755 intro N
756 let dpf := genuineZetaDerivedPhaseFamily sensor qlf horder
757 let A : ℝ := Real.log Constants.phi * (π * |(-sensor.charge : ℤ)| / 4)
758 let C : ℝ :=
759 qlf.logDerivBound * qlf.radius * (2 * π) *
760 (Real.log Constants.phi * Real.sinh A)
761 have hA_nonneg : 0 ≤ A := by
762 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
763 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
764 have hbase_nonneg : 0 ≤ π * |(-sensor.charge : ℤ)| / 4 := by
765 positivity
766 dsimp [A]
767 exact mul_nonneg hlog_nonneg hbase_nonneg
768 have hC_nonneg : 0 ≤ C := by
769 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
770 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
771 have hsinh_nonneg : 0 ≤ Real.sinh A := (Real.sinh_nonneg_iff).2 hA_nonneg
772 have hlinconst_nonneg : 0 ≤ Real.log Constants.phi * Real.sinh A := by
773 exact mul_nonneg hlog_nonneg hsinh_nonneg
774 have hpref_nonneg : 0 ≤ qlf.logDerivBound * qlf.radius * (2 * π) := by
775 have h2pi_nonneg : 0 ≤ (2 * π : ℝ) := by positivity
776 exact mul_nonneg (mul_nonneg qlf.logDerivBound_pos.le qlf.radius_pos.le) h2pi_nonneg
777 dsimp [C]
778 exact mul_nonneg hpref_nonneg hlinconst_nonneg
779 have hterm :
780 ∀ n : Fin N,
781 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
782 ∑ j : Fin (8 * (n.val + 1)),
783 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
784 (n.val + 1) j|
785 ≤ C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2)) := by
786 intro n
787 have hk_pos : (0 : ℝ) < (n.val : ℝ) + 1 := by positivity
788 have ht0 : 0 ≤ (1 : ℝ) / ((n.val : ℝ) + 1) := by
789 exact div_nonneg (by norm_num) hk_pos.le
790 have hk_one_le : (1 : ℝ) ≤ (n.val : ℝ) + 1 := by
791 have hn_nonneg : (0 : ℝ) ≤ n.val := by exact_mod_cast (Nat.zero_le n.val)
792 linarith
793 have ht1 : (1 : ℝ) / ((n.val : ℝ) + 1) ≤ 1 := by
794 exact div_le_self (show (0 : ℝ) ≤ 1 by norm_num) hk_one_le
795 have hpure :
796 |defectPhasePureIncrement dpf (n.val + 1)| =
797 (π * |(-sensor.charge : ℤ)| / 4) / ((n.val : ℝ) + 1) := by
798 simpa [dpf, Nat.cast_add] using
799 genuine_pure_increment_abs_eq sensor qlf horder (n.val + 1) (Nat.succ_pos n.val)
800 have harg :
801 Real.log Constants.phi * |defectPhasePureIncrement dpf (n.val + 1)| =
802 ((1 : ℝ) / ((n.val : ℝ) + 1)) * A := by
803 rw [hpure]
804 dsimp [A]
805 have hk_ne : (n.val : ℝ) + 1 ≠ 0 := by positivity
806 field_simp [hk_ne]
807 have hsinh_scale :
808 Real.sinh (((1 : ℝ) / ((n.val : ℝ) + 1)) * A) ≤
809 ((1 : ℝ) / ((n.val : ℝ) + 1)) * Real.sinh A :=
810 sinh_mul_le_mul_sinh ht0 ht1 hA_nonneg
811 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
812 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
813 have hsinh_nonneg : 0 ≤ Real.sinh A := (Real.sinh_nonneg_iff).2 hA_nonneg
814 have hcoeff_nonneg :
815 0 ≤ (Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1)) := by
816 exact mul_nonneg (mul_nonneg hlog_nonneg hsinh_nonneg) ht0
817 have hlin :
818 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| ≤
819 (Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1)) := by
820 rw [phiCostLinearCoeff, harg]
821-- ... 145 more lines elided ...