OAI/NumberTheory/EgyptianFractions/BadPredecessorCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.indexed_predecessor_count line 11

   Source documentation

   An indexed bipartite degree count. Repeated values of the maps retain separate indices in I, exactly as required by the divisor descent.

   theorem indexed_predecessor_count
       {α β ι : Type*} [DecidableEq α] [DecidableEq β] [DecidableEq ι]
       (U : Finset α) (H : Finset β) (I : Finset ι)
       (r : ι → α → β) (w : ι → β → ℝ) (L : ℝ) (hL : 0 < L)
       (hleft : ∀ u ∈ U, L ≤ ((I.filter (fun i => r i u ∈ H)).card : ℝ))
       (hright : ∀ i ∈ I, ∀ h ∈ H,
         ((U.filter (fun u => r i u = h)).card : ℝ) ≤ w i h) :
       (U.card : ℝ) ≤ (∑ i ∈ I, ∑ h ∈ H, w i h) / L := by
   …

2. theorem OAI.Problem337.indexed_predecessor_count_with_exceptions line 39

   Source documentation

   The degree count with an inherited set and an exceptional set removed.

   theorem indexed_predecessor_count_with_exceptions
       {α β ι : Type*} [DecidableEq α] [DecidableEq β] [DecidableEq ι]
       (S E B U : Finset α) (H : Finset β) (I : Finset ι)
       (r : ι → α → β) (w : ι → β → ℝ) (L : ℝ) (hL : 0 < L)
       (hcover : S ⊆ E ∪ B ∪ U)
       (hleft : ∀ u ∈ U, L ≤ ((I.filter (fun i => r i u ∈ H)).card : ℝ))
       (hright : ∀ i ∈ I, ∀ h ∈ H,
         ((U.filter (fun u => r i u = h)).card : ℝ) ≤ w i h) :
       (S.card : ℝ) ≤ (E.card : ℝ) + (B.card : ℝ) +
         (∑ i ∈ I, ∑ h ∈ H, w i h) / L := by
   …

3. theorem OAI.Problem337.descent_bad_predecessor_count line 62

   Source documentation

   The exact finite combinatorial inequality used to propagate bad numerators. H is the current bad set, Hnext the next bad set, and E the Fourier exception set. Fibers may be bounded by truncated divisor counts.

   theorem descent_bad_predecessor_count
       {ι : Type*} [DecidableEq ι]
       (H Hnext E : Finset ℕ) (I : Finset ι) (Y : ℝ) (ρ : ℝ)
       (r : ι → ℕ → ℕ) (w : ι → ℕ → ℝ)
       (hρ : 0 < ρ) (hI : I.Nonempty)
       (hinherit : ∀ u ∈ H, (u : ℝ) ≤ Y → u ∈ Hnext)
       (hleft : ∀ u ∈ H, u ∉ E → Y < (u : ℝ) →
         ρ * (I.card : ℝ) / 2 ≤ ((I.filter (fun i => r i u ∈ Hnext)).card : ℝ))
       (hright : ∀ i ∈ I, ∀ h ∈ Hnext,
         ((H.filter (fun u => r i u = h)).card : ℝ) ≤ w i h) :
       (H.card : ℝ) ≤ (E.card : ℝ) + (Hnext.card : ℝ) +
         (2 / (ρ * (I.card : ℝ))) * (∑ i ∈ I, ∑ h ∈ Hnext, w i h) := by
   …

4. theorem OAI.Problem337.predecessor_fiber_le_divisors line 104

   Source documentation

   A fiber of a residue map consists of divisors of the shifted numerator.

   theorem predecessor_fiber_le_divisors
       (H : Finset ℕ) (X : ℝ) (N h : ℕ) (r : ℕ → ℕ)
       (hN : 0 < N) (hX : ∀ u ∈ H, (u : ℝ) ≤ X)
       (hdiv : ∀ u ∈ H, u ∣ N + r u) :
       (H.filter (fun u => r u = h)).card ≤
         ((N + h).divisors.filter (fun u : ℕ => (u : ℝ) ≤ X)).card := by
   …

5. theorem OAI.Problem337.descent_bad_predecessor_divisor_count line 122

   Source documentation

   The manuscript's bad-pair inequality, with actual truncated divisor counts.

   theorem descent_bad_predecessor_divisor_count
       {ι : Type*} [DecidableEq ι]
       (H Hnext E : Finset ℕ) (I : Finset ι) (X Y ρ : ℝ)
       (r : ι → ℕ → ℕ) (N : ι → ℕ)
       (hρ : 0 < ρ) (hI : I.Nonempty)
       (hX : ∀ u ∈ H, (u : ℝ) ≤ X)
       (hN : ∀ i ∈ I, 0 < N i)
       (hdiv : ∀ i ∈ I, ∀ u ∈ H, u ∣ N i + r i u)
       (hinherit : ∀ u ∈ H, (u : ℝ) ≤ Y → u ∈ Hnext)
       (hleft : ∀ u ∈ H, u ∉ E → Y < (u : ℝ) →
         ρ * (I.card : ℝ) / 2 ≤ ((I.filter (fun i => r i u ∈ Hnext)).card : ℝ)) :
       (H.card : ℝ) ≤ (E.card : ℝ) + (Hnext.card : ℝ) +
   …