mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
fix(lean): BlockCoprimeDensity round-3 fixes
Adds: - D_finite_eq_prod_saturated_mul_active (product decomposition thm) - saturatedPart/activePart definitions with partition and disjointness - localFactor_pos, D_finite_pos (positivity theorems) Fixes: - field_simp replaced with simpler hx + field_simp [hx] in C_finite_zero_eq_one - Docstring 'positive integer' → 'natural number' - Removed unnecessary simp, by_cases cleanup - @[simp] kept only on C_finite_zero_eq_one (unconditional) - Simpler proofs for saturatedPart_union/disjoint using Finset.filter/Subset
This commit is contained in:
parent
d2eb6a74c4
commit
44fcafe0de
1 changed files with 107 additions and 14 deletions
|
|
@ -10,9 +10,11 @@ natural density is (analytically) known to be:
|
|||
WHAT IS FORMALIZED:
|
||||
• Finite truncation D_G(n) = ∏_{p ≤ G} (1 − min(n+1, p) / p²) (ℚ)
|
||||
• Saturation partition: when p ≤ n+1 the factor simplifies to 1−1/p
|
||||
• Decomposition into product over saturated × active primes
|
||||
• C_G(n) = (∏_{p ≤ G} (1−1/p²)⁻¹) · D_G(n), with C_G(0) = 1 exact
|
||||
• Boundary value at n=1 (Feller-Tornier product)
|
||||
• Positivity of D_G(n) and the local factors
|
||||
• Complementarity of saturated/active primes
|
||||
• Boundary value at n=1 (Feller-Tornier product)
|
||||
• Eval witnesses for small G
|
||||
|
||||
WHAT IS NOT FORMALIZED (analytic number theory, beyond scope):
|
||||
|
|
@ -24,9 +26,11 @@ WHAT IS NOT FORMALIZED (analytic number theory, beyond scope):
|
|||
Structure:
|
||||
§1 Local factor and saturation partition
|
||||
§2 Finite Euler product D_G(n)
|
||||
§3 Boundary values at n=0, n=1 and the ζ(2) cancellation
|
||||
§4 Notes on analytic extensions (unformalized)
|
||||
§5 Eval witnesses
|
||||
§3 Product decomposition into saturated/active primes
|
||||
§4 Boundary values at n=0, n=1 and the ζ(2) cancellation
|
||||
§5 Positivity theorems
|
||||
§6 Notes on analytic extensions (unformalized)
|
||||
§7 Eval witnesses
|
||||
|
||||
References:
|
||||
- Wessen Getachew, "C(n) — Block-Coprime Density"
|
||||
|
|
@ -73,7 +77,7 @@ def isActive (n p : ℕ) : Prop :=
|
|||
instance (n p : ℕ) : Decidable (isActive n p) :=
|
||||
inferInstanceAs (Decidable (n + 1 < p))
|
||||
|
||||
/-- Every positive integer is either saturated or active at block length n. -/
|
||||
/-- Every natural number is either saturated or active at block length n. -/
|
||||
theorem isSaturated_or_isActive (n p : ℕ) : isSaturated n p ∨ isActive n p := by
|
||||
by_cases h : p ≤ n + 1
|
||||
· left; exact h
|
||||
|
|
@ -84,7 +88,7 @@ theorem isSaturated_iff_not_isActive (n p : ℕ) : isSaturated n p ↔ ¬isActiv
|
|||
unfold isSaturated isActive
|
||||
exact ⟨Nat.not_lt.mpr, Nat.le_of_not_gt⟩
|
||||
|
||||
/-- For a saturated prime (p ≤ n+1), the local factor simplifies to 1 − 1/p.
|
||||
/-- For saturated p (p ≤ n+1), the local factor simplifies to 1 − 1/p.
|
||||
Since min(n+1, p) = p, we have 1 − p/p² = 1 − 1/p. -/
|
||||
theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n p = 1 - (1 : ℚ) / (p : ℚ) := by
|
||||
unfold isSaturated at h
|
||||
|
|
@ -95,7 +99,7 @@ theorem localFactor_saturated (n p : ℕ) (h : isSaturated n p) : localFactor n
|
|||
· simp [hzero]
|
||||
· field_simp [hzero]
|
||||
|
||||
/-- For an active prime (p > n+1), the local factor is 1 − (n+1)/p².
|
||||
/-- For active p (p > n+1), the local factor is 1 − (n+1)/p².
|
||||
Since min(n+1, p) = n+1, this is immediate from the definition. -/
|
||||
theorem localFactor_active (n p : ℕ) (h : isActive n p) : localFactor n p = 1 - ((n+1 : ℕ) : ℚ) / ((p : ℚ) ^ 2) := by
|
||||
unfold isActive at h
|
||||
|
|
@ -131,7 +135,69 @@ def C_finite (n G : ℕ) : ℚ :=
|
|||
(Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * D_finite n G
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §3 Boundary values and the ζ(2) cancellation
|
||||
-- §3 Product decomposition into saturated/active primes
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
/-- The saturated subset of primesUpTo G at block length n. -/
|
||||
def saturatedPart (n G : ℕ) : Finset ℕ :=
|
||||
(primesUpTo G).filter (fun p => decide (isSaturated n p))
|
||||
|
||||
/-- The active subset of primesUpTo G at block length n. -/
|
||||
def activePart (n G : ℕ) : Finset ℕ :=
|
||||
(primesUpTo G).filter (fun p => decide (isActive n p))
|
||||
|
||||
/-- The saturated and active parts partition primesUpTo G. -/
|
||||
lemma saturatedPart_union_activePart (n G : ℕ) : saturatedPart n G ∪ activePart n G = primesUpTo G := by
|
||||
apply Finset.Subset.antisymm
|
||||
· intro p hp
|
||||
rcases Finset.mem_union.1 hp with (hp' | hp')
|
||||
· exact (Finset.mem_filter.1 hp').1
|
||||
· exact (Finset.mem_filter.1 hp').1
|
||||
· intro p hp
|
||||
rcases isSaturated_or_isActive n p with (h_sat | h_act)
|
||||
· apply Finset.mem_union_left
|
||||
refine Finset.mem_filter.mpr ⟨hp, ?_⟩
|
||||
exact decide_eq_true h_sat
|
||||
· apply Finset.mem_union_right
|
||||
refine Finset.mem_filter.mpr ⟨hp, ?_⟩
|
||||
exact decide_eq_true h_act
|
||||
|
||||
/-- The saturated and active parts are disjoint. -/
|
||||
lemma saturatedPart_disjoint_activePart (n G : ℕ) : Disjoint (saturatedPart n G) (activePart n G) := by
|
||||
rw [Finset.disjoint_iff_inter_eq_empty]
|
||||
by_contra hne
|
||||
have h_nonempty : (saturatedPart n G ∩ activePart n G).Nonempty := by
|
||||
rw [Finset.nonempty_iff_ne_empty]
|
||||
exact hne
|
||||
rcases h_nonempty with ⟨p, hp⟩
|
||||
rcases Finset.mem_inter.1 hp with ⟨hp_sat, hp_act⟩
|
||||
have hp_sat_pair := Finset.mem_filter.mp (by simpa [saturatedPart] using hp_sat)
|
||||
have hp_act_pair := Finset.mem_filter.mp (by simpa [activePart] using hp_act)
|
||||
have hp_sat_pure : isSaturated n p := hp_sat_pair.2
|
||||
have hp_act_pure : isActive n p := hp_act_pair.2
|
||||
unfold isSaturated at hp_sat_pure
|
||||
unfold isActive at hp_act_pure
|
||||
omega
|
||||
|
||||
/-- D_finite(n, G) decomposes into a product over saturated primes times a
|
||||
product over active primes. Applying `localFactor_saturated` and
|
||||
`localFactor_active` to each factor gives the explicit form:
|
||||
|
||||
D_finite n G = (∏_{saturated} (1 − 1/p)) · (∏_{active} (1 − (n+1)/p²)) -/
|
||||
theorem D_finite_eq_prod_saturated_mul_active (n G : ℕ) : D_finite n G =
|
||||
(Finset.prod (saturatedPart n G) (fun p => localFactor n p)) *
|
||||
(Finset.prod (activePart n G) (fun p => localFactor n p)) := by
|
||||
unfold D_finite
|
||||
calc
|
||||
Finset.prod (primesUpTo G) (fun p => localFactor n p)
|
||||
= Finset.prod (saturatedPart n G ∪ activePart n G) (fun p => localFactor n p) := by
|
||||
rw [saturatedPart_union_activePart]
|
||||
_ = (Finset.prod (saturatedPart n G) (fun p => localFactor n p)) *
|
||||
(Finset.prod (activePart n G) (fun p => localFactor n p)) := by
|
||||
rw [Finset.prod_union (saturatedPart_disjoint_activePart n G)]
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §4 Boundary values and the ζ(2) cancellation
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
/-- For n=0, every prime is active (since the smallest prime is 2 > 1).
|
||||
|
|
@ -161,12 +227,14 @@ lemma D_finite_zero_eq (G : ℕ) : D_finite 0 G = Finset.prod (primesUpTo G) (fu
|
|||
have h : ∀ p ∈ primesUpTo G, (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹ * (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) = 1 := by
|
||||
intro p hp
|
||||
have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2
|
||||
have hp_pos : p ≠ 0 := Nat.Prime.ne_zero hp_prime
|
||||
have hp_sq_ne_zero : (p : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 (by exact_mod_cast hp_pos)
|
||||
have hp_sq_minus_one_ne_zero : (p : ℚ) ^ 2 - 1 ≠ 0 := by
|
||||
have hp_sq_ne_zero : (p : ℚ) ^ 2 ≠ 0 := pow_ne_zero 2 (by exact_mod_cast (Nat.Prime.ne_zero hp_prime))
|
||||
have hx : (1 - (1 : ℚ) / ((p : ℚ) ^ 2)) ≠ 0 := by
|
||||
have hp_gt_one : (p : ℚ) > 1 := by exact_mod_cast (Nat.Prime.one_lt hp_prime)
|
||||
have hp_sq_gt_one : (p : ℚ) ^ 2 > 1 := by nlinarith
|
||||
have hp_sq_pos : 0 < (p : ℚ) ^ 2 := by nlinarith
|
||||
have hdiv : (1 : ℚ) / ((p : ℚ) ^ 2) < 1 := (div_lt_one hp_sq_pos).mpr hp_sq_gt_one
|
||||
nlinarith
|
||||
field_simp [hp_sq_ne_zero, hp_sq_minus_one_ne_zero]
|
||||
field_simp [hx]
|
||||
calc
|
||||
(Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) * D_finite 0 G
|
||||
= (Finset.prod (primesUpTo G) (fun p => (1 - (1 : ℚ) / ((p : ℚ) ^ 2))⁻¹)) *
|
||||
|
|
@ -200,7 +268,32 @@ lemma D_finite_one_eq (G : ℕ) : D_finite 1 G = Finset.prod (primesUpTo G) (fun
|
|||
simp [localFactor_one_prime p hp_prime]
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §4 Notes on analytic extensions (unformalized)
|
||||
-- §5 Positivity
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
/-- For a prime p ≥ 2, the local factor is strictly positive. -/
|
||||
lemma localFactor_pos (n p : ℕ) (hp : Nat.Prime p) : localFactor n p > 0 := by
|
||||
unfold localFactor
|
||||
have hp_gt_one : (p : ℚ) > 1 := by exact_mod_cast (Nat.Prime.one_lt hp)
|
||||
have hp_sq_gt_one : (p : ℚ) ^ 2 > 1 := by nlinarith
|
||||
have hp_sq_pos : 0 < (p : ℚ) ^ 2 := by nlinarith
|
||||
have h_num_le_denom : (min (n+1) p : ℚ) < (p : ℚ) ^ 2 := by
|
||||
calc
|
||||
(min (n+1) p : ℚ) ≤ (p : ℚ) := by exact_mod_cast Nat.min_le_right (n+1) p
|
||||
_ < (p : ℚ) ^ 2 := by nlinarith
|
||||
have h_div_lt_one : (min (n+1) p : ℚ) / ((p : ℚ) ^ 2) < 1 :=
|
||||
(div_lt_one hp_sq_pos).mpr h_num_le_denom
|
||||
nlinarith
|
||||
|
||||
/-- D_G(n) is strictly positive for any G. -/
|
||||
theorem D_finite_pos (n G : ℕ) : D_finite n G > 0 := by
|
||||
unfold D_finite
|
||||
refine Finset.prod_pos fun p hp => ?_
|
||||
have hp_prime : Nat.Prime p := (Finset.mem_filter.mp hp).2
|
||||
exact localFactor_pos n p hp_prime
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §6 Notes on analytic extensions (unformalized)
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
/-
|
||||
|
|
@ -229,7 +322,7 @@ identification as a density is not proven here.
|
|||
-/
|
||||
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
-- §5 Eval witnesses
|
||||
-- §7 Eval witnesses
|
||||
-- ═══════════════════════════════════════════════════════════════════════════
|
||||
|
||||
-- D_G(0) at G=31 (first 11 primes): ∏_{p ≤ 31} (1 − 1/p²) ≈ 0.61174
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue