feat(NumberTheory/ArithmeticStatistics/Reducible): Counting reducible polynomials

[khwilson]

A result of van der Waerden critical in arithmetic statistics which shows that the number of reducible monic polynomials of degree n is O(H^(n-1)).

---

[github-actions]

PR summary 0dd5d5f56a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
14 files Mathlib.Data.Set.Card.Arithmetic Mathlib.Data.Set.Card Mathlib.Data.Set.PowersetCard Mathlib.Data.Setoid.Partition.Card Mathlib.GroupTheory.ClassEquation Mathlib.GroupTheory.Perm.DomMulAct Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.Subsingleton Mathlib.Order.Height Mathlib.Order.Hom.PowersetCard Mathlib.Order.Interval.Set.Nat Mathlib.SetTheory.Cardinal.Embedding Mathlib.SetTheory.Cardinal.NatCount	1
Mathlib.NumberTheory.ArithmeticStatistics.Reducible (new file)	3117

---

Declarations diff

+ Asymptotics.isBigO_pow_pow_atTop_of_le
+ boxPolyₘ
+ card_mahlerMeasure_monic
+ card_mahlerMeasure_monic_le_pow
+ encard_image2_le
+ exists_monic_factors_of_not_irreducible
+ finite_mahlerMeasure_monic_le
+ finite_monicBoxPoly
+ finite_monicBoxPolyReducible
+ finite_monicBoxPolyReducibleₘ
+ finite_monicBoxPolyₘ
+ isBigO_monicBoxPolyReducible_2
+ mem_monicBoxPoly
+ mem_monicBoxPolyₘ
+ monicBoxPoly
+ monicBoxPolyReducible
+ monicBoxPolyReducible_subset_biUnion
+ monicBoxPolyReducible_subset_monicBoxPoly
+ monicBoxPolyReducible_subset_monicBoxPolyReducibleₘ
+ monicBoxPolyReducibleₘ
+ monicBoxPolyReducibleₘ_subset_monicBoxPolyReducible
+ monicBoxPolyReducibleₘ_subset_monicBoxPolyₘ
+ monicBoxPoly_empty_lt_one
+ monicBoxPoly_subset_monicBoxPolyₘ
+ monicBoxPolyₘ
+ monicBoxPolyₘ_subset_monicBoxPoly
+ ncard_image2_le
+ ncard_monicBoxPoly
+ ncard_monicBoxPoly_le
+ ncard_monicBoxPoly_lt_one

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6902	1	backward.isDefEq.respectTransparency

Current commit cda7e0cb01
Reference commit 0dd5d5f56a

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).