PopulatedKernelSelection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Retaining entire populated kernel fibers

theorem OAI.Ostmann.small_kernel_fibers_card line 13
Source documentation
Fibers smaller than the cutoff remove at most the number of kernels times that cutoff. The estimate concerns actual endpoint populations.
```
theorem small_kernel_fibers_card (S : Finset ℤ) (f : ℤ → ℤ) (Q : ℕ) :
    (S.filter fun x => (S.filter fun y => f y = f x).card < Q).card ≤
      (S.image f).card * Q := by
…
```

def OAI.Ostmann.populatedKernelPoints line 32

Source documentation

The retained set is a union of entire original fibers.

def populatedKernelPoints (S : Finset ℤ) (f : ℤ → ℤ) (A : ℤ → Prop)
    [DecidablePred A] (Q : ℕ) : Finset ℤ :=
…

theorem OAI.Ostmann.populatedKernelPoints_subset line 36
theorem OAI.Ostmann.populatedKernelPoints_loss line 40
theorem OAI.Ostmann.populatedKernelPoints_fiber line 60

theorem OAI.Ostmann.exists_nonexceptional_endpoint_pair line 76

Source documentation

A strict population surplus supplies an actual nonexceptional endpoint pair.

theorem exists_nonexceptional_endpoint_pair (S T : Finset ℤ) (f g : ℤ → ℤ)
    (E : ℤ → Prop) [DecidablePred E] (M : ℝ)
    (hbad : (((S.product T).filter fun z => E (f z.1 * g z.2)).card : ℝ) ≤ M)
    (hlarge : M < (S.card : ℝ) * T.card) :
    ∃ x ∈ S, ∃ y ∈ T, ¬ E (f x * g y) := by
…

theorem OAI.Ostmann.exists_populated_kernel_pair line 92

Source documentation

A bound on the exceptional endpoint pairs, smaller than the retained product, gives two complete populated fibers outside the exceptional family.

theorem exists_populated_kernel_pair (S T : Finset ℤ) (f g : ℤ → ℤ)
    (A B : ℤ → Prop) [DecidablePred A] [DecidablePred B] (Q : ℕ)
    (E : ℤ → Prop) [DecidablePred E] (M : ℝ)
    (hbad : (((S.product T).filter fun z => E (f z.1 * g z.2)).card : ℝ) ≤ M)
    (hlarge : M < ((populatedKernelPoints S f A Q).card : ℝ) *
      (populatedKernelPoints T g B Q).card) :
    ∃ u ∈ S.image f, ∃ v ∈ T.image g, A u ∧ B v ∧ ¬ E (u * v) ∧
      Q ≤ (S.filter fun x => f x = u).card ∧ Q ≤ (T.filter fun y => g y = v).card := by
…

Mentions: OAI.Ostmann.populatedKernelPoints