OAI/NumberTheory/EgyptianFractions/DensityLoss.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.descent_bad_predecessor_divisor_count_loss line 12

   Source documentation

   The bad-predecessor bound permits a polynomial loss in the lower degree; indexed multiplicities and the actual truncated divisor fibers are retained.

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

2. theorem OAI.Problem337.descent_recurrence_of_pair_and_moment_loss line 39

   Source documentation

   Moment normalization with a general loss factor. A polynomial loss can be absorbed by the separately proved exponential coefficient estimate.

   theorem descent_recurrence_of_pair_and_moment_loss
       (a B T X Y ρ ε E r J P : ℝ) (hX : 0 < X) (hρ : 0 < ρ)
       (hρ1 : ρ ≤ 1) (hJ : 0 < J) (hP : 0 ≤ P) (hY : Y = ρ * X)
       (hB0 : 0 ≤ B) (hBY : B ≤ Y) (hr : 1 < r)
       (hcoeff : 1 + P * Real.exp (E / r) ≤ Real.exp (2 * E))
       (hpair : a ≤ X * ε + B + (P / (ρ * J)) * T)
       (hsum : T ≤ J * (Y * Real.exp (E / r) * (B / Y) ^ (1 - 1 / r))) :
       a / X ≤ ε + Real.exp (2 * E) * (B / Y) ^ (1 - 1 / r) := by
   …