diff --git a/LeanEval/Combinatorics/PartitionAsymptotics.lean b/LeanEval/Combinatorics/PartitionAsymptotics.lean new file mode 100644 index 0000000..858e7e9 --- /dev/null +++ b/LeanEval/Combinatorics/PartitionAsymptotics.lean @@ -0,0 +1,20 @@ +import EvalTools.Markers +import Mathlib.Analysis.Asymptotics.Defs +import Mathlib.Combinatorics.Enumerative.Partition.Basic +import Mathlib.Analysis.Complex.Exponential +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic + +/-! # Asymptotic expression for the number of integer partitions + +Hardy and Ramanujan's asymptotic expression for the number of integer partitions. + +G. H. Hardy, S. Ramanujan. *Asymptotic formulae in combinatory analysis*, 1918. +-/ + +open Asymptotics Filter Fintype + +/-- Hardy and Ramanujan's asymptotic formula. -/ +@[eval_problem] +theorem isEquivalent_card_partition : + (fun (n : ℕ) => (card n.Partition : ℝ)) ~[atTop] + (fun n => Real.exp (Real.pi * Real.sqrt (2 * n / 3)) / (4 * n * Real.sqrt 3)) := sorry diff --git a/manifests/problems.toml b/manifests/problems.toml index b9e42d1..1a82bc7 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -646,6 +646,16 @@ holes = ["neukirch_uchida"] submitter = "Junyan Xu" source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1." +[[problem]] +id = "asymptotic_partition" +title = "Hardy-Ramanujan asymptotic formula for the number of integer partitions" +test = false +module = "LeanEval.Combinatorics.PartitionAsymptotics" +holes = ["isEquivalent_card_partition"] +submitter = "Thomas K Waring" +source = "G. H. Hardy, S. Ramanujan. *Asymptotic formulae in combinatory analysis*, 1918." +informal_solution = "Evaluate the growth-rate of coefficients in the generating function by the so-called circle method." + [[problem]] id = "balanceable_bounded_partitions" title = "Balanceable k-bounded partitions"