feat(Analysis/Complex): Hadamard quotient #34328
Conversation
PR 1 of the Hadamard Factorization pipeline Co-authored by Jonathan Washburn and Matteo Cipollina
pr 2 of the HadamardFactorization pipeline Co-authored by Jonathan Washburn and Matteo Cipollina
PR 1 of the Hadamard Factorization pipeline Co-authored by Jonathan Washburn and Matteo Cipollina
…thlib4 into CartanProductBound
feat(Analysis/Complex): Hadamard quotient
github-actions
bot
added
the
new-contributor
PR summary 18ef4ef4f3
|
| Files | Import difference |
|---|---|
Mathlib.Topology.Algebra.InfiniteSum.GroupWithZero (new file) |
833 |
Mathlib.Topology.MetricSpace.Annulus (new file) |
970 |
Mathlib.MeasureTheory.Constructions.BorelSpace.Annulus (new file) |
1459 |
Mathlib.Analysis.Meromorphic.DivisorSupport (new file) |
1793 |
Mathlib.Analysis.Complex.CartanBound (new file) |
2454 |
Mathlib.Analysis.Complex.WeierstrassFactor (new file) |
2455 |
Mathlib.Analysis.Complex.CartanInverseFactorBound (new file) |
2461 |
Mathlib.Analysis.Complex.BorelCaratheodory (new file) |
2477 |
Mathlib.Analysis.Complex.ExpPoly (new file) |
2482 |
Mathlib.Analysis.Complex.ExpPoly.Growth (new file) |
2483 |
Mathlib.Analysis.Complex.CanonicalProduct (new file) |
2499 |
Mathlib.Analysis.Complex.DivisorIndex (new file) |
2510 |
Mathlib.Analysis.Complex.DivisorConvergence (new file) Mathlib.Analysis.Complex.DivisorUnits (new file) |
2511 |
Mathlib.Analysis.Complex.DivisorFiber (new file) |
2513 |
Mathlib.Analysis.Complex.DivisorComplement (new file) |
2514 |
Mathlib.Analysis.Complex.DivisorPartialProductFactor (new file) |
2515 |
Mathlib.Analysis.Complex.DivisorQuotientConvergence (new file) |
2516 |
Mathlib.Analysis.Complex.DivisorQuotientRemovable (new file) |
2517 |
Mathlib.Analysis.Complex.Divisor (new file) |
2519 |
Mathlib.Analysis.Complex.CartanMajorantBound (new file) |
2525 |
Mathlib.Analysis.Complex.HadamardFactorization (new file) |
2609 |
Declarations diff
+ Cφ
+ Cφ_pos
+ HasProd.inv₀
+ K
+ K_nonneg
+ TendstoUniformlyOn.mul_left_bounded
+ ae_restrict_norm_phi_le_of_forall_mem
+ analyticAt_update_limUnder_divisorCanonicalProduct_div_pow
+ analyticOrderAt_finset_prod_weierstrassFactor_divisorZeroIndex₀
+ analyticOrderAt_ne_top_of_exists_ne_zero
+ analyticOrderAt_partialProduct_eq_fiberCard_of_subset
+ analyticOrderAt_prod_fiberFinset
+ analyticOrderAt_weierstrassFactor_div_self
+ analyticOrderNatAt_divisorCanonicalProduct_eq_analyticOrderNatAt
+ analyticOrderNatAt_divisorCanonicalProduct_eq_fiber_card
+ analyticOrderNatAt_divisorCanonicalProduct_zero
+ analyticOrderNatAt_finset_prod_weierstrassFactor_divisorZeroIndex₀
+ analyticOrderNatAt_hadamardDenom_eq
+ analyticOrderNatAt_prod_fiberFinset
+ analyticOrderNatAt_weierstrassFactor_div_self
+ annulusIcc
+ annulusIcc_eq
+ annulusIcc_eq_empty
+ annulusIcc_mono
+ annulusIcc_subset_closedBall
+ annulusIcc_union_annulusIoc
+ annulusIcc_union_annulusIoi
+ annulusIcc_union_annulusIoo
+ annulusIci
+ annulusIci_eq
+ annulusIco
+ annulusIco_eq
+ annulusIco_eq_empty
+ annulusIco_mono
+ annulusIco_subset_ball
+ annulusIco_union_annulusIcc
+ annulusIco_union_annulusIci
+ annulusIco_union_annulusIco
+ annulusIoc
+ annulusIoc_eq
+ annulusIoc_eq_empty
+ annulusIoc_mono
+ annulusIoc_subset_closedBall
+ annulusIoc_union_annulusIoc
+ annulusIoc_union_annulusIoi
+ annulusIoc_union_annulusIoo
+ annulusIoi
+ annulusIoi_eq
+ annulusIoo
+ annulusIoo_eq
+ annulusIoo_eq_empty
+ annulusIoo_mono
+ annulusIoo_subset_ball
+ annulusIoo_union_annulusIcc
+ annulusIoo_union_annulusIci
+ annulusIoo_union_annulusIco
+ bddAbove_norm_divisorCanonicalProduct_div_pow_puncturedBall
+ canonicalProduct
+ canonicalProduct_converges_uniformOn_compact
+ cartan_card_small_le
+ cartan_majorant_nonneg
+ cartan_majorant_summable
+ cartan_rpow_mul_le
+ cartan_sum_majorant_le
+ differentiableOn_divisorCanonicalProduct_div_pow_sub
+ differentiableOn_divisorCanonicalProduct_univ
+ differentiableOn_divisorComplementCanonicalProduct_univ
+ differentiableOn_divisorPartialProduct_div_pow_sub
+ differentiableOn_update_limUnder_divisorCanonicalProduct_div_pow
+ differentiable_hadamardDenom
+ differentiable_partialLogSum
+ differentiable_weierstrassFactor
+ divisorCanonicalProduct
+ divisorCanonicalProduct_eq_zero_at_index
+ divisorCanonicalProduct_eq_zero_of_exists
+ divisorCanonicalProduct_ne_zero_at_zero
+ divisorCanonicalProduct_zero
+ divisorComplementCanonicalProduct
+ divisorComplementCanonicalProduct_ne_zero_at
+ divisorComplementFactor
+ divisorComplementPartialProduct
+ divisorComplementPartialProduct_def
+ divisorComplementPartialProduct_ne_zero_on_ball
+ divisorPartialProduct
+ divisorPartialProduct_def
+ divisorPartialProduct_eq_fiber_mul_complement_of_subset
+ divisorPartialProduct_ne_zero_on_ball_punctured
+ divisorZeroIndex
+ divisorZeroIndex₀
+ divisorZeroIndex₀_fiberFinset
+ divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt
+ divisorZeroIndex₀_fiberFinset_card_eq_toNat_divisor
+ divisorZeroIndex₀_fiber_finite
+ divisorZeroIndex₀_norm_le_finite
+ divisorZeroIndex₀_val
+ divisorZeroIndex₀_val_eq_of_mem_ball
+ divisorZeroIndex₀_val_mem_divisor_support
+ divisorZeroIndex₀_val_mem_divisor_support'
+ divisorZeroIndex₀_val_ne_zero
+ divisor_hadamardDenom_eq
+ divisor_hadamardQuotient_eq_zero
+ divisor_support_countable
+ divisor_support_discrete
+ divisor_support_inter_compact_finite
+ divisor_univ_eq_analyticOrderNatAt_int
+ eannulusIcc
+ eannulusIcc_eq_empty
+ eannulusIcc_eq_preimage
+ eannulusIcc_mono
+ eannulusIcc_ofReal
+ eannulusIci
+ eannulusIci_eq_preimage
+ eannulusIci_ofReal
+ eannulusIco
+ eannulusIco_eq_empty
+ eannulusIco_eq_preimage
+ eannulusIco_mono
+ eannulusIco_ofReal
+ eannulusIoc
+ eannulusIoc_eq_empty
+ eannulusIoc_eq_preimage
+ eannulusIoc_mono
+ eannulusIoc_ofReal
+ eannulusIoi
+ eannulusIoi_eq_preimage
+ eannulusIoi_ofReal
+ eannulusIoo
+ eannulusIoo_eq_empty
+ eannulusIoo_eq_preimage
+ eannulusIoo_mono
+ eannulusIoo_ofReal
+ eq_mul_div_one_add_of_eq_div_sub
+ eventually_atTop_subset_fiberFinset
+ eventually_eq_fiber_mul_divisorComplementPartialProduct
+ eventually_eq_punctured_quotient_of_factorization
+ eventually_exists_analyticAt_eq_pow_smul_divisorComplementPartialProduct
+ eventually_exists_analyticAt_eq_pow_smul_divisorPartialProduct
+ eventually_exists_ball_eq_punctured_quotient_of_factorization
+ exists_analyticAt_eq_pow_smul_of_partialProduct_contains_fiber
+ exists_ball_divisorComplementCanonicalProduct_ne_zero
+ exists_ball_eq_divisorCanonicalProduct_div_pow_eq
+ exists_ball_inter_divisor_support_eq_singleton
+ exists_ball_inter_divisor_support_eq_singleton_of_index
+ exists_entire_nonzero_hadamardQuotient
+ exists_nonzero_seq_divisor_support_diff_zero
+ exists_pow_eq_complex
+ exists_radius_Ioc_sum_mul_phi_div_le_Cφ_mul_sum
+ exists_radius_Ioc_sum_mul_phi_div_le_Cφ_mul_sum_avoid
+ exists_seq_eq_range_divisor_support
+ exists_z_norm_eq_re_eval_ge
+ finite_divisorZeroIndex₀_subtype_norm_le
+ hadamardDenom
+ hadamardDenom_ne_zero_at
+ hasProdLocallyUniformlyOn_divisorCanonicalProduct_univ
+ hasProdLocallyUniformlyOn_divisorComplementCanonicalProduct_univ
+ hasProdUniformlyOn_divisorCanonicalProduct_univ
+ hasProdUniformlyOn_divisorComplementCanonicalProduct_univ
+ hasProd_norm_inv_le_exp_of_pointwise_le_exp
+ iUnion_Ico_map_succ_eq_Ici
+ iUnion_Ioc_map_succ_eq_Ioi
+ iUnion_annulusIco_eq_annulusIci
+ iUnion_annulusIoc_eq_annulusIoi
+ integral_phi_div_le_Cφ_mul
+ integral_phi_le_Cφ_mul
+ intervalIntegrable_phi_div
+ intervalIntegrable_phi_dyadic
+ intervalIntegrable_sqrt_two_div_abs_one_sub_Icc
+ logTail
+ log_norm_one_sub_div_ge_neg_phi
+ log_norm_weierstrassFactor_ge_log_norm_one_sub_sub
+ log_norm_weierstrassFactor_ge_neg_two_pow
+ max_one_norm_div_pow_le_one_add_rpow
+ measurableSet_annulusIcc
+ measurableSet_annulusIci
+ measurableSet_annulusIco
+ measurableSet_annulusIoc
+ measurableSet_annulusIoi
+ measurableSet_annulusIoo
+ measurableSet_eannulusIcc
+ measurableSet_eannulusIci
+ measurableSet_eannulusIco
+ measurableSet_eannulusIoc
+ measurableSet_eannulusIoi
+ measurableSet_eannulusIoo
+ measurable_phi
+ mem_divisorZeroIndex₀_fiberFinset
+ mem_divisorZeroIndex₀_fiberFinset_iff_val_mem_ball
+ mem_divisorZeroIndex₀_fiberFinset_of_val_mem_ball
+ mul_conj_div_norm
+ natDegree_le_floor_of_growth_exp_eval
+ neg_log_le_sqrt_two_div
+ neg_log_one_sub_eq_tsum
+ neg_posLog_inv_le_log
+ no_zero_on_sphere_of_forall_val_norm_ne
+ norm_inv_weierstrassFactor_le_exp_far
+ norm_inv_weierstrassFactor_le_exp_near
+ norm_logTail_le
+ norm_lt_norm_two_mul_sub
+ norm_pow_div_one_sub_le_two
+ norm_two_mul_div_one_add_le
+ not_mem_divisorZeroIndex₀_fiberFinset_iff_val_ne
+ pairwise_disjoint_on_annulusIco_succ
+ pairwise_disjoint_on_annulusIoc_succ
+ pairwise_disjoint_on_annulusIoo_succ
+ pairwise_disjoint_on_eannulusIco_succ
+ pairwise_disjoint_on_eannulusIoc_succ
+ pairwise_disjoint_on_eannulusIoo_succ
+ partialLogSum
+ partialLogSum_zero
+ phi_eq_zero_of_one_le_abs_one_sub
+ phi_le_log_two_of_le_half
+ posLog_one_div_abs_one_sub_le_sqrt_two_div
+ posLog_one_div_norm_one_sub_le_posLog_one_div_abs_one_sub
+ posLog_one_div_norm_one_sub_le_posLog_one_div_abs_one_sub_norm
+ prod_le_exp_sum
+ schwarz_applied
+ summable_logTail
+ tendstoLocallyUniformlyOn_divisorComplementPartialProduct_univ
+ tendstoLocallyUniformlyOn_divisorPartialProduct_div_pow_sub
+ tendstoLocallyUniformlyOn_divisorPartialProduct_univ
+ tendstoUniformlyOn_divisorPartialProduct_div_pow_sub
+ val_not_mem_ball_of_not_mem_fiberFinset
+ weierstrassFactor
+ weierstrassFactorUnits
+ weierstrassFactorUnits_coe
+ weierstrassFactor_at_one
+ weierstrassFactor_at_zero
+ weierstrassFactor_div_ne_zero_on_ball_of_not_mem_fiberFinset
+ weierstrassFactor_div_ne_zero_on_ball_of_val_ne
+ weierstrassFactor_div_ne_zero_on_ball_punctured
+ weierstrassFactor_eq_exp_neg_tail
+ weierstrassFactor_eq_zero_iff
+ weierstrassFactor_ne_zero_iff
+ weierstrassFactor_ne_zero_of_ne_one
+ weierstrassFactor_sub_one_pow_bound
+ weierstrassFactor_zero
+ zero_free_polynomial_growth_is_exp_poly
+ φ
+ φ_le_sqrt
+ φ_nonneg
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (1.00, 0.25)
| Current number | Change | Type |
|---|---|---|
| 4 | 1 | maxHeartBeats modifications |
Current commit 4f26e827d8
Reference commit 18ef4ef4f3
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
jonwashburn
changed the title
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
4 participants
PR 15 towards Hadamard Factorization
Co-authored-by: Matteo Cipollina matteo.cipollina@yahoo.it