IndisputableMonolith.NumberTheory.EulerInstantiation

declarations in this module (81)

• def Primes L56
• def PrimeSum L60
• def HilbertSchmidtNormSq L66
• theorem hilbert_schmidt_convergent L72
• theorem eigenvalue_lt_one L78
• theorem eigenvalue_pos L85
• def det2Factor L94
• def det2LogFactor L101
• theorem det2_log_factor_bound L107
• theorem det2_log_summable L134
• theorem det2_product_convergent L175
• def carrierLog L184
• def carrierValue L189
• theorem carrier_log_convergent L193
• theorem carrier_pos L198
• theorem carrier_nonvanishing L206
• def carrierDerivTerm L215
• def carrierDerivBound L220
• theorem carrierDerivTerm_nonneg L224
• theorem carrierDerivBound_summable L241
• theorem carrierDerivBound_finite L298
• theorem carrierDerivBound_pos L302
• theorem carrier_zeta_identity L324
• theorem zeros_in_continuation L333
• def primeLog L342
• def eulerPrimePowerComplex L347
• def eulerDet2FactorComplex L352
• def eulerPrimeLogDerivTermComplex L358
• def zetaReciprocal L364
• def defectSensorCenter L370
• def defectSensorCirclePoint L376
• def zetaReciprocalOnSensorCircle L380
• theorem defectSensorCirclePoint_re L385
• theorem defectSensorCirclePoint_mem_strip L392
• theorem norm_eulerPrimePowerComplex L402
• theorem norm_eulerPrimePowerComplex_lt_one L422
• theorem norm_eulerPrimePowerComplex_lt_one_on_sensorCircle L438
• theorem one_sub_eulerPrimePowerComplex_ne_zero L450
• theorem eulerDet2FactorComplex_ne_zero L462
• theorem zetaReciprocal_differentiableAt L472
• theorem norm_eulerPrimePowerComplex_eq_rpow L481
• theorem norm_eulerPrimeLogDerivTermComplex_le L490
• theorem norm_form_eq_carrierDerivTerm L510
• theorem norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm L522
• theorem eulerPrimeLogDerivTermComplex_summable L535
• theorem analyticAt_riemannZeta L546
• theorem zetaReciprocal_meromorphicAt L555
• theorem meromorphicOrderAt_zetaReciprocal L562
• theorem zetaReciprocal_order_at_zero L570
• structure remembers L579
• structure WitnessedDefectSensor L581
• theorem zetaReciprocal_local_factorization L612
• def eulerQuantitativeFactorization L624
• theorem eulerQuantitativeFactorization_logDerivBound L658
• theorem eulerQuantitativeFactorization_center L668
• theorem eulerQuantitativeFactorization_order L678
• def eulerCarrierInstance L691
• def eulerRegularCarrier L702
• theorem euler_regular_carrier_covers_strip L712
• def EulerBudgetUpgradeTarget L722
• theorem euler_budget_upgrade_extends_regular L729
• def eulerZeroTrace L740
• def eulerBudgetedCarrier L750
• theorem euler_budget_upgrade_target L767
• def eulerCostCoveringPackage L772
• theorem argument_principle_sampling L786
• def DeprecatedDefectAnnularCostBounded L815
• theorem defect_annular_cost_bounded_inconsistent L826
• theorem rh_from_complex_analysis_axioms L842
• theorem rh_no_zeros_in_strip L852
• theorem defect_bounded_impossible L862
• def zetaDefectSensor L876
• theorem sensor_carrier_compatible L886
• structure EulerInstantiationCert L902
• def mkEulerInstantiationCert L921
• theorem euler_rh_conditional L936
• theorem riemann_hypothesis_euler_conditional L943
• def eulerSampledBudgetedCarrier L959
• theorem eulerSampledBudgetedCarrier_scale_zero L969
• def eulerSampledPackage L974

… and 1 more