Import erdos1196 formalization

LeanPool.lean

@@ -29,6 +29,20 @@ import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.OneSidedBarrier
 import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.ResolventBound
 import LeanPool.ArchonFirstProofResults.FirstProof6.Problem6
 import LeanPool.Basic
+import LeanPool.Erdos1196
+import LeanPool.Erdos1196.Basic
+import LeanPool.Erdos1196.FirstEntryRowTerm
+import LeanPool.Erdos1196.FormalConjecturesErdos1196
+import LeanPool.Erdos1196.HitMass
+import LeanPool.Erdos1196.Main
+import LeanPool.Erdos1196.Markov
+import LeanPool.Erdos1196.Normalization
+import LeanPool.Erdos1196.NormalizationCore
+import LeanPool.Erdos1196.NormalizationSmallPrime
+import LeanPool.Erdos1196.Preliminaries
+import LeanPool.Erdos1196.PreliminariesMertens
+import LeanPool.Erdos1196.PreliminariesTailAux
+import LeanPool.Erdos1196.PrimitiveWeight
 import LeanPool.FelConjecture
 import LeanPool.FelConjecture.Solution
 import LeanPool.RamanujanTauMissesPrimes

LeanPool/Erdos1196.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2026 Math Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Math Inc.
+-/
+
+import LeanPool.Erdos1196.Basic
+import LeanPool.Erdos1196.Preliminaries
+import LeanPool.Erdos1196.Markov
+import LeanPool.Erdos1196.PrimitiveWeight
+import LeanPool.Erdos1196.HitMass
+import LeanPool.Erdos1196.Main
+import LeanPool.Erdos1196.FormalConjecturesErdos1196
+
+/-!
+# Primitive Sets Above x (Erdős Problem 1196)
+
+Source: url:https://github.com/math-inc/Erdos1196
+Authors: Math Inc.
+Status: verified
+Main declarations: `PrimitiveSetsAboveX.mainTheorem`, `Erdos1196.erdos_1196`
+Tags: number-theory, combinatorics, analysis
+-/
+
+/-!
+## Mathematical overview
+
+A set `A ⊆ ℕ` is *primitive* if no element of `A` divides another. This development proves
+that every primitive set `A ⊆ ℕ ∩ [x, ∞)` satisfies
+`∑_{a ∈ A} 1 / (a log a) ≤ 1 + O(1 / log x)` as `x → ∞`, the quantitative form of Erdős
+Problem `#1196`. The argument builds an explicit sub-Markov chain on the divisibility poset
+whose visiting probabilities are proportional to `1 / (n log n)`; the first-hit mass of a
+primitive set is then at most `1`, and the normalization estimate for the constant `B_x`
+converts this into the logarithmic-series bound.
+
+The exported modules follow the structure of the proof: arithmetic and tail estimates
+(`LeanPool.Erdos1196.Preliminaries`), the normalization decomposition of `B_x`
+(`LeanPool.Erdos1196.Markov`), the Markov-layer and hit-mass arguments
+(`LeanPool.Erdos1196.HitMass`), the final quantitative theorem
+`PrimitiveSetsAboveX.mainTheorem` (`LeanPool.Erdos1196.Main`), and the
+`formal-conjectures`-style theorem `Erdos1196.erdos_1196`
+(`LeanPool.Erdos1196.FormalConjecturesErdos1196`).
+
+## Provenance
+
+Imported from <https://github.com/math-inc/Erdos1196>. Upstream contains no `sorry`s.
+Ported from Lean `v4.30.0-rc1` to Lean Pool's `v4.30.0-rc2`.
+-/

LeanPool/Erdos1196/Basic.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Math Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Math Inc.
+-/
+import Mathlib.Algebra.Notation.Indicator
+import Mathlib.NumberTheory.Chebyshev
+import Mathlib.Topology.Algebra.InfiniteSum.Real
+
+/-!
+# Basic definitions for primitive sets above `x`
+
+This file introduces the core objects used throughout the development: the arithmetic sums
+appearing in the analytic estimates, the entry weights and normalization data `b_x`, `B_x`,
+and `μ_x`, and the abstract Markov-layer interface used for the visit-probability argument.
+
+## Main definitions
+
+* `PrimitiveSet`
+* `mertensPartialSum`
+* `tailSum`
+* `ry`
+* `entryWeight`
+* `normalizationConstant`
+* `initialDistribution`
+* `MarkovLayer`
+-/
+
+open scoped ArithmeticFunction BigOperators
+
+namespace PrimitiveSetsAboveX
+
+/-- The primitive-set predicate used throughout the local development. -/
+def PrimitiveSet (A : Set ℕ) : Prop :=
+  ∀ ⦃m n : ℕ⦄, m ∈ A → n ∈ A → m ∣ n → m = n
+
+/-- Partial sums of `Λ(q) / q`. -/
+noncomputable def mertensPartialSum (t : ℕ) : ℝ :=
+  (Finset.Icc 1 t).sum fun q => Λ q / (q : ℝ)
+
+/-- The logarithmic tail sum `T(m, y)` used in the normalization estimates. -/
+noncomputable def tailSum (m y : ℕ) : ℝ :=
+  ∑' q : ℕ,
+    if y ≤ q then
+      Λ q / ((q : ℝ) * (Real.log ((m * q : ℕ) : ℝ)) ^ 2)
+    else 0
+
+/-- The quantity `R_Y(m)` introduced in the proof of the main theorem. -/
+noncomputable def ry (Y m : ℕ) : ℝ :=
+  ∑' q : ℕ,
+    if Y ≤ q then
+      (Real.log (m : ℝ) / (Real.log ((m * q : ℕ) : ℝ)) ^ 2) * (Λ q / (q : ℝ))
+    else 0
+
+/-- The transition weight `p(m, mq)` of the sub-Markov chain. -/
+noncomputable def transitionWeight (Y m q : ℕ) : ℝ :=
+  if Y ≤ q then
+    (Real.log (m : ℝ) / (Real.log ((m * q : ℕ) : ℝ)) ^ 2) * (Λ q / (q : ℝ))
+  else 0
+
+/-- The entry weight `b_x(n)` used to define the initial distribution of the chain. -/
+noncomputable def entryWeight (x Y n : ℕ) : ℝ :=
+  1 / ((n : ℝ) * (Real.log (n : ℝ)) ^ 2) *
+    (((n.divisors.filter (fun q => q < Y)).sum fun q => Λ q) +
+      ((n.divisors.filter (fun q => Y ≤ q ∧ n / q < x)).sum fun q => Λ q))
+
+/-- The normalizing constant `B_x`. -/
+noncomputable def normalizationConstant (x Y : ℕ) : ℝ :=
+  ∑' n : ℕ, if x ≤ n then entryWeight x Y n else 0
+
+/-- The normalized initial distribution `μ_x(n) = b_x(n) / B_x`. -/
+noncomputable def initialDistribution (x Y n : ℕ) : ℝ :=
+  entryWeight x Y n / normalizationConstant x Y
+
+/--
+An abstract sub-Markov layer on the state space `n ≥ x`, together with a candidate
+visit-probability function satisfying the last-jump recurrence.
+-/
+structure MarkovLayer (x Y : ℕ) where
+  /-- The transition weights satisfy the required sub-Markov row-sum bound. -/
+  transitionSubMarkov :
+    ∀ ⦃m : ℕ⦄, x ≤ m → (∑' q : ℕ, transitionWeight Y m q) ≤ 1
+  /-- The probability that the chain ever visits `n` when started from `μ_x`. -/
+  visitProbability : ℕ → ℝ
+  /-- The last-jump recurrence for the visiting probabilities. -/
+  visitProbabilityRecurrence :
+    ∀ ⦃n : ℕ⦄, x ≤ n →
+      visitProbability n =
+        initialDistribution x Y n +
+          ∑' q : ℕ,
+            if Y ≤ q ∧ q ∣ n ∧ x ≤ n / q then
+              visitProbability (n / q) * transitionWeight Y (n / q) q
+            else 0
+
+end PrimitiveSetsAboveX

LeanPool/Erdos1196/FirstEntryRowTerm.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Math Inc. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Math Inc.
+-/
+import LeanPool.Erdos1196.Basic
+import Mathlib.Algebra.Order.Floor.Div
+
+/-!
+# First-entry row data
+
+This file packages the row-wise data for the first-entry contribution to the normalization
+constant. It introduces the threshold selecting admissible first jumps from a parent state `m`,
+the resulting tail sum, and the pairwise weights used later in the fiberwise reindexing of
+`B_x`.
+
+## Main definitions
+
+* `entryThreshold`
+* `firstEntryTail`
+* `firstEntryPairWeight`
+-/
+
+open scoped ArithmeticFunction BigOperators
+
+namespace PrimitiveSetsAboveX
+
+/-- The least threshold satisfying both `q ≥ Y` and `x ≤ m * q`. -/
+def entryThreshold (x Y m : ℕ) : ℕ :=
+  max Y (x ⌈/⌉ m)
+
+/-- The first-entry tail sum starting from a parent state `m`. -/
+noncomputable def firstEntryTail (x Y m : ℕ) : ℝ :=
+  ∑' q : ℕ,
+    if entryThreshold x Y m ≤ q then
+      Λ q / ((q : ℝ) * (Real.log ((m * q : ℕ) : ℝ)) ^ 2)
+    else 0
+
+/-- The pairwise weight indexed by a parent state `m` and jump factor `q`
+for the first-entry contribution to `B_x`. -/
+noncomputable def firstEntryPairWeight (x Y : ℕ) (mq : ℕ × ℕ) : ℝ :=
+  if 1 ≤ mq.1 ∧ mq.1 < x ∧ entryThreshold x Y mq.1 ≤ mq.2 then
+    Λ mq.2 / (((mq.1 * mq.2 : ℕ) : ℝ) * (Real.log ((mq.1 * mq.2 : ℕ) : ℝ)) ^ 2)
+  else 0
+
+/-- The lower-threshold condition is exactly the conjunction `q ≥ Y` and `x ≤ m * q`. -/
+lemma entryThreshold_le_iff (x Y m q : ℕ) (hm : 0 < m) :
+    entryThreshold x Y m ≤ q ↔ Y ≤ q ∧ x ≤ m * q := by
+  rw [entryThreshold, max_le_iff]
+  constructor
+  · rintro ⟨hY, hq⟩
+    exact ⟨hY, (ceilDiv_le_iff_le_mul hm).1 hq⟩
+  · rintro ⟨hY, hxq⟩
+    exact ⟨hY, (ceilDiv_le_iff_le_mul hm).2 hxq⟩
+
+/-- For a parent state already known to satisfy `1 ≤ m < x`, the pairwise first-entry weight is
+the corresponding scaled tail summand. -/
+lemma firstEntryPairWeight_eq {x Y m q : ℕ} (hm1 : 1 ≤ m) (hmx : m < x) :
+    firstEntryPairWeight x Y (m, q) =
+      (1 / (m : ℝ)) *
+        (if entryThreshold x Y m ≤ q then
+          Λ q / ((q : ℝ) * (Real.log ((m * q : ℕ) : ℝ)) ^ 2)
+        else 0) := by
+  by_cases hq : entryThreshold x Y m ≤ q
+  · rw [firstEntryPairWeight, if_pos ⟨hm1, hmx, hq⟩, if_pos hq]
+    rw [Nat.cast_mul, div_eq_mul_inv, div_eq_mul_inv]
+    ring_nf
+  · rw [firstEntryPairWeight, if_neg, if_neg hq]
+    · simp
+    · exact fun h => hq h.2.2
+
+/-- For a fixed parent state `m`, the first-entry row is either the scaled tail summand row when
+`1 ≤ m < x`, or identically zero otherwise. -/
+lemma firstEntryPairWeight_row (x Y m : ℕ) :
+    (fun q : ℕ => firstEntryPairWeight x Y (m, q)) =
+      if 1 ≤ m ∧ m < x then
+        fun q : ℕ =>
+          (1 / (m : ℝ)) *
+            (if entryThreshold x Y m ≤ q then
+              Λ q / ((q : ℝ) * (Real.log ((m * q : ℕ) : ℝ)) ^ 2)
+            else 0)
+      else fun _ : ℕ => 0 := by
+  by_cases hm : 1 ≤ m ∧ m < x
+  · rcases hm with ⟨hm1, hmx⟩
+    funext q
+    simp [firstEntryPairWeight_eq (x := x) (Y := Y) (m := m) (q := q) hm1 hmx, hm1, hmx]
+  · funext q
+    by_cases hm1 : 1 ≤ m
+    · have hmx : ¬ m < x := by
+        intro hmx
+        exact hm ⟨hm1, hmx⟩
+      simp [firstEntryPairWeight, hm1, hmx]
+    · simp [firstEntryPairWeight, hm1]
+
+end PrimitiveSetsAboveX