Opening the checked source with Lean hover information.
FourExponentials.NormalizedConjecture
HardyZeta.criticalPoint_injective
HardyZeta.criticalPoint_ne_zero
HardyZeta.criticalPoint_ne_one
HardyZeta.continuous_criticalPoint
HardyZeta.completedZeta_criticalPoint_eq_zero_iff
HardyZeta.criticalXi_eq_zero_iff
HardyZeta.continuous_criticalXi
HardyZeta.InfinitelyManyCriticalZeros
HardyZeta.ZerosAboveEveryHeight
HardyZeta.infinite_criticalZeros_of_zerosAboveEveryHeight
HardyZeta.integrable_exp_neg_abs
HardyZeta.differenceMultiplier
HardyZeta.modifiedDifference_cos
HardyZeta.modifiedDifference_cosh
HardyZeta.differenceMultiplier_nonneg
HardyZeta.modifiedDifference_const_mul
HardyZeta.iterate_modifiedDifference_cosh
HardyZeta.differenceMultiplier_eq_squares
HardyZeta.tendsto_differenceMultiplier_div_sq
HardyZeta.modifiedDifference_integral
HardyZeta.integrable_difference_kernel
HardyZeta.abs_modifiedDifference_le
HardyZeta.abs_iterate_modifiedDifference_le
HardyZeta.continuous_dslope_sinh
HardyZeta.continuous_dslope_sin
HardyZeta.extendedDifferenceMultiplier
HardyZeta.extendedDifferenceMultiplier_zero
HardyZeta.continuous_extendedDifferenceMultiplier
HardyZeta.extendedDifferenceMultiplier_eq
HardyZeta.tendsto_integral_differenceKernel_Icc
HardyZeta.tendsto_scaled_boundary_value
HardyZeta.tendsto_scaled_iterate_modifiedDifference
HardyZeta.tendsto_thetaBoundaryRemainder_re_weighted
HardyZeta.tendsto_scaled_theta_difference
HardyZeta.difference_sample_bounds
HardyZeta.integrableOn_hardyDifference
HardyZeta.iterate_hardyTransform_eq_integral
HardyZeta.iterate_modifiedDifference_congr_strip
HardyZeta.not_eventually_positive_hardyWeight_mul
HardyZeta.zerosAboveEveryHeight
HardyZeta.iterate_modifiedDifference_sub
HardyZeta.iterate_modifiedDifference_const_mul
HardyZeta.iterate_modifiedDifference_cos_succ
HardyZeta.iterate_hardyTransform_eq_theta
HardyZeta.eventually_difference_center_inside
HardyZeta.tendsto_scaled_hardy_difference
HardyZeta.normalizedHardyKernel
HardyZeta.normalizedHardyKernel_nonneg
HardyZeta.normalizedHardyIntegral_eq
HardyZeta.tendsto_normalizedHardyIntegral
HardyZeta.integrableOn_normalizedHardyKernel
HardyZeta.continuous_hardyWeight
HardyZeta.integrableOn_hardyWeight_cosh
HardyZeta.abs_hardyWeight_le_abs
HardyZeta.integrable_hardyWeight_exp
HardyZeta.integral_shifted_even_power
HardyZeta.integral_shifted_even_power_eq_zero
HardyZeta.not_geometric_domination
HardyZeta.mellin_conj_of_real_kernel
HardyZeta.compact_tail_le_total_add_initial
HardyZeta.continuous_normalizedHardyKernel
HardyZeta.tendsto_compact_normalizedHardyKernel
HardyZeta.boundary_compact_comparison
HardyZeta.initial_polynomial_bound
HardyZeta.tail_polynomial_bound
HardyZeta.not_positive_tail_of_compact_moments
HardyZeta.not_positive_tail_of_vanishing_differences
HardyZeta.differentiableAt_psi
HardyZeta.psi_ofReal_eq_evenKernel
HardyZeta.thetaFourierIntegrand
HardyZeta.norm_thetaFourierIntegrand
HardyZeta.differentiableAt_thetaFourierIntegrand
HardyZeta.integrable_thetaFourierIntegrand_horizontal
HardyZeta.norm_thetaFourierIntegrand_le
HardyZeta.norm_theta_verticalIntegral_le
HardyZeta.tendsto_theta_verticalIntegral
HardyZeta.thetaFourierIntegral_shift
HardyZeta.thetaHorizontalMass_nonneg
HardyZeta.norm_thetaFourierIntegral_le
HardyZeta.completedZeta_eq_thetaFourierIntegral
HardyZeta.norm_completedZeta_critical_le
HardyZeta.norm_psi_cusp_le_exp
HardyZeta.re_reciprocal_four_mul
HardyZeta.sector_reciprocal_lower
HardyZeta.norm_psi_cusp_le_sector
HardyZeta.weighted_norm_psi_cusp_le_sector
HardyZeta.tendsto_weighted_psi_cusp
HardyZeta.fourier_theta_horizontal_eq_integral
HardyZeta.thetaFourierIntegrand_horizontal
HardyZeta.fourier_theta_horizontal
HardyZeta.fourier_theta_eq_hardyWeight
HardyZeta.fourier_theta_horizontal_eq_weight
HardyZeta.integrable_fourier_theta_horizontal
HardyZeta.integral_fourier_theta_horizontal
HardyZeta.integral_hardyWeight_exp
HardyZeta.integral_hardyWeight_exp_eq_cosh
HardyZeta.integral_hardyWeight_cosh
HardyZeta.norm_thetaLogKernel_le_of_re_nonneg
HardyZeta.norm_thetaLogKernel_le
HardyZeta.integrable_thetaLogKernel_horizontal
HardyZeta.hasDerivAt_thetaCuspPath_zero
HardyZeta.tendsto_thetaCuspPath_div
HardyZeta.tendsto_thetaCuspPath
HardyZeta.eventually_thetaCuspPath_sector
HardyZeta.tendsto_thetaCuspPath_weighted
HardyZeta.tendsto_theta_argument_weighted
HardyZeta.thetaBoundaryRemainder
HardyZeta.norm_thetaBoundaryRemainder
HardyZeta.tendsto_thetaBoundaryRemainder_weighted
HardyZeta.modifiedThetaLogKernel
HardyZeta.modifiedTheta_mellinConvergent
HardyZeta.completedZeta₀_eq_fourier
HardyZeta.completedZeta_eq_fourier
HardyZeta.integrable_mellinLogKernel
HardyZeta.integrable_modifiedThetaLogKernel
HardyZeta.integrable_poleLogKernel
HardyZeta.fourier_poleLogKernel
HardyZeta.correctedThetaLogKernel
HardyZeta.integrable_correctedThetaLogKernel
HardyZeta.fourier_sub_of_integrable
HardyZeta.completedZeta_eq_fourier_corrected
HardyZeta.correctedThetaLogKernel_eq
HardyZeta.correctedThetaLogKernel_ae_eq
HardyZeta.integrable_thetaLogKernel
HardyZeta.completedZeta_eq_fourier_theta
HardyZeta.differentiableAt_thetaLogKernel
HardyZeta.finite_zeros_in_bounded_interval
HardyZeta.constant_sign_on_Ioi
HardyZeta.eventual_sign_of_not_zerosAboveEveryHeight
SharpFiveExponentials.Conjecture
HardyZeta.thetaFourierIntegrand.eq_1
HardyZeta.criticalXi_eq_zero_iff._simp_1_7
HardyZeta.thetaHorizontalMass.eq_1
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_3
HardyZeta.extendedDifferenceMultiplier._proof_2
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_1
HardyZeta.integrableOn_normalizedHardyKernel._simp_1_1
HardyZeta.fourier_poleLogKernel._simp_1_4
HardyZeta.differenceMultiplier.eq_1
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_2
HardyZeta.eventually_thetaCuspPath_sector._simp_1_5
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_7
HardyZeta.fourier_poleLogKernel._simp_1_5
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_6
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_6
HardyZeta.correctedThetaLogKernel.eq_1
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_6
HardyZeta.compact_tail_le_total_add_initial._simp_1_1
HardyZeta.criticalXi_eq_zero_iff._simp_1_3
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_1
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_4
HardyZeta.tendsto_scaled_boundary_value._simp_1_2
HardyZeta.thetaStripConstant._proof_1
HardyZeta.eventually_thetaCuspPath_sector._simp_1_1
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_5
HardyZeta.integrableOn_normalizedHardyKernel._simp_1_2
HardyZeta.eventually_thetaCuspPath_sector._simp_1_2
HardyZeta.criticalXi_eq_zero_iff._simp_1_5
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_7
HardyZeta.fourier_poleLogKernel._simp_1_1
HardyZeta.normalizedHardyIntegral_eq._simp_1_1
HardyZeta.tendsto_scaled_boundary_value._simp_1_3
HardyZeta.normalizedHardyKernel._proof_1
HardyZeta.thetaTerm_shift._simp_1_1
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_7
HardyZeta.fourier_poleLogKernel._simp_1_2
HardyZeta.normalizedHardyKernel.eq_1
HardyZeta.completedZeta_criticalPoint_eq_zero_iff._simp_1_1
HardyZeta.eventually_thetaCuspPath_sector._simp_1_6
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_5
HardyZeta.thetaCuspPath._proof_1
HardyZeta.normalizedHardyIntegral_eq._simp_1_2
HardyZeta.extendedDifferenceMultiplier.eq_1
HardyZeta.eventually_thetaCuspPath_sector._simp_1_7
HardyZeta.eventually_thetaCuspPath_sector._simp_1_4
HardyZeta.fourier_poleLogKernel._simp_1_3
HardyZeta.fourier_poleLogKernel._simp_1_6
HardyZeta.compact_tail_le_total_add_initial._simp_1_2
HardyZeta.criticalXi_eq_zero_iff._simp_1_4
HardyZeta.criticalXi_eq_zero_iff._simp_1_6
HardyZeta.modifiedThetaLogKernel.eq_1
HardyZeta.eventually_thetaCuspPath_sector._simp_1_3
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_3
HardyZeta.criticalPoint._proof_1
HardyZeta.modifiedThetaLogKernel._proof_1
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_2
HardyZeta.tendsto_scaled_boundary_value._simp_1_7
HardyZeta.thetaLogKernel._proof_1
HardyZeta.modifiedDifference._proof_1
HardyZeta.not_positive_tail_of_compact_moments._simp_1_1
HardyZeta.integrable_exp_neg_abs._simp_1_1
HardyZeta.hardyWeight._proof_1
HardyZeta.modifiedDifference.eq_1
HardyZeta.psi_shift._proof_1_1
HardyZeta.thetaBoundaryRemainder.eq_1
HardyZeta.tendsto_scaled_boundary_value._simp_1_1
HardyZeta.extendedDifferenceMultiplier._proof_1
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_4
SharpFiveExponentials.Conjecture._proof_1
HardyZeta.fourier_poleLogKernel._simp_1_7
HardyZeta.extendedDifferenceMultiplier_eq._simp_1_2
HardyZeta.tendsto_scaled_boundary_value._simp_1_6
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_5
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_4
HardyZeta.not_eventually_positive_hardyWeight_mul._simp_1_1
HardyZeta.fourier_theta_eq_hardyWeight._simp_1_1
HardyZeta.zerosAboveEveryHeight._simp_1_1
HardyZeta.completedZeta_eq_thetaFourierIntegral._simp_1_3