feat(Analysis/Complex) cartan majorant bound #34327
Conversation
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
feat(Analysis/Complex) cartan majorant bound
github-actions
bot
added
the
new-contributor
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
PR summary 18ef4ef4f3
|
| Files | Import difference |
|---|---|
Mathlib.Topology.MetricSpace.Annulus (new file) |
970 |
Mathlib.MeasureTheory.Constructions.BorelSpace.Annulus (new file) |
1459 |
Mathlib.Analysis.Complex.CartanBound (new file) |
1665 |
Mathlib.Analysis.Meromorphic.DivisorSupport (new file) |
1793 |
Mathlib.Analysis.Complex.WeierstrassFactor (new file) |
2455 |
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) |
2521 |
Declarations diff
+ Cφ
+ Cφ_pos
+ TendstoUniformlyOn.mul_left_bounded
+ 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_finset_prod_weierstrassFactor_divisorZeroIndex₀
+ 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_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_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
+ 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_nonzero_seq_divisor_support_diff_zero
+ exists_seq_eq_range_divisor_support
+ finite_divisorZeroIndex₀_subtype_norm_le
+ hasProdLocallyUniformlyOn_divisorCanonicalProduct_univ
+ hasProdLocallyUniformlyOn_divisorComplementCanonicalProduct_univ
+ hasProdUniformlyOn_divisorCanonicalProduct_univ
+ hasProdUniformlyOn_divisorComplementCanonicalProduct_univ
+ iUnion_Ico_map_succ_eq_Ici
+ iUnion_Ioc_map_succ_eq_Ioi
+ iUnion_annulusIco_eq_annulusIci
+ iUnion_annulusIoc_eq_annulusIoi
+ logTail
+ log_norm_weierstrassFactor_ge_log_norm_one_sub_sub
+ log_norm_weierstrassFactor_ge_neg_two_pow
+ measurableSet_annulusIcc
+ measurableSet_annulusIci
+ measurableSet_annulusIco
+ measurableSet_annulusIoc
+ measurableSet_annulusIoi
+ measurableSet_annulusIoo
+ measurableSet_eannulusIcc
+ measurableSet_eannulusIci
+ measurableSet_eannulusIco
+ measurableSet_eannulusIoc
+ measurableSet_eannulusIoi
+ measurableSet_eannulusIoo
+ mem_divisorZeroIndex₀_fiberFinset
+ mem_divisorZeroIndex₀_fiberFinset_iff_val_mem_ball
+ mem_divisorZeroIndex₀_fiberFinset_of_val_mem_ball
+ neg_log_one_sub_eq_tsum
+ norm_logTail_le
+ norm_pow_div_one_sub_le_two
+ 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
+ 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
+ φ
+ φ_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 6a6d1deabf
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).
jonwashburn
changed the title
🚨 PR Title Needs FormattingPlease update the title to match our commit style conventions. Errors from script: Details on the required title formatThe title should fit the following format:
|
4 participants
PR 12 of the Hadamard Factorization pipeline
Co-authored with Matteo Cipollina (matteo.cipollina@yahoo.it)