CommonCenter.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Extracting one common center

The finite incidence argument in Section 3: large matching-prime sets with small pairwise intersections have total size at most twice the ambient set. A large moment therefore forces one large matching set.

def OAI.Ostmann.centerIncidence line 20
theorem OAI.Ostmann.sum_centerIncidence line 23
theorem OAI.Ostmann.sum_centerIncidence_sq line 32

theorem OAI.Ostmann.commonCenter_incidence_bound line 57

Source documentation

Incidence Cauchy--Schwarz, with the diagonal separated before estimating intersections.

theorem commonCenter_incidence_bound {I P : Type*} [Fintype I] [Fintype P]
    [DecidableEq P] (S : I → Finset P) (K : ℝ) (hK : 0 ≤ K)
    (hinter : ∀ i j, i ≠ j → ((S i ∩ S j).card : ℝ) ≤ K) :
    (∑ i : I, ((S i).card : ℝ)) ^ 2 ≤
      (Fintype.card P : ℝ) *
        ((∑ i : I, ((S i).card : ℝ)) + K * (Fintype.card I : ℝ) ^ 2) := by
…

theorem OAI.Ostmann.commonCenter_total_le_twice line 86

Source documentation

The quantitative absorption used for the high matching sets.

theorem commonCenter_total_le_twice {R J b A K : ℝ}
    (hJ : 0 ≤ J) (hb : 0 ≤ b) (hA : 0 < A)
    (hinc : R ^ 2 ≤ J * (R + K * b ^ 2))
    (hlarge : b * A ≤ R) (hsmall : 2 * K * J ≤ A ^ 2) : R ≤ 2 * J := by
…

theorem OAI.Ostmann.commonCenter_family_total_le_twice line 95

theorem OAI.Ostmann.exists_commonCenter_of_moment line 109

Source documentation

A lower moment and the total incidence budget force a single large center.

theorem exists_commonCenter_of_moment {I P : Type*} [Fintype I] [Fintype P]
    [DecidableEq P] [Nonempty I] (S : I → Finset P) (A K L : ℝ) (k : ℕ)
    (hA : 0 < A) (hK : 0 ≤ K)
    (hlarge : ∀ i, A ≤ ((S i).card : ℝ))
    (hinter : ∀ i j, i ≠ j → ((S i ∩ S j).card : ℝ) ≤ K)
    (hsmall : 2 * K * (Fintype.card P : ℝ) ≤ A ^ 2)
    (hmoment : L ≤ ∑ i : I, ((S i).card : ℝ) ^ (k + 1)) :
    ∃ i : I, L ≤ 2 * (Fintype.card P : ℝ) * ((S i).card : ℝ) ^ k := by
…