OAI/NumberTheory/EgyptianFractions/DiscreteFirstDerivative.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.ExponentialSum.phase line 8
2. def OAI.Problem337.ExponentialSum.phaseWeight line 10
3. lemma OAI.Problem337.ExponentialSum.phase_norm line 13
4. lemma OAI.Problem337.ExponentialSum.phase_add line 16
5. lemma OAI.Problem337.ExponentialSum.cot_antitone_unit line 23
6. lemma OAI.Problem337.ExponentialSum.sin_pi_lower line 40
7. lemma OAI.Problem337.ExponentialSum.abs_cot_pi_le line 55
8. lemma OAI.Problem337.ExponentialSum.phaseWeight_identity line 63
9. lemma OAI.Problem337.ExponentialSum.phaseWeight_norm_le line 81
10. lemma OAI.Problem337.ExponentialSum.phaseWeight_difference_norm line 94
11. lemma OAI.Problem337.ExponentialSum.phase_step_weight line 106
12. lemma OAI.Problem337.ExponentialSum.weighted_telescope line 121

    Source documentation

    Summation by parts for a sequence whose differences have a reciprocal weight.

    lemma weighted_telescope (z w : ℕ → ℂ) (N : ℕ)
        (hstep : ∀ i < N, (z (i + 1) - z i) * w i = z i) :
        (∑ i ∈ Finset.range N, z i) = z N * w N - z 0 * w 0 +
          ∑ i ∈ Finset.range N, z (i + 1) * (w i - w (i + 1)) := by
    …

13. lemma OAI.Problem337.ExponentialSum.weighted_telescope_succ line 136

    Source documentation

    Endpoint-efficient form: the last weight is attached to the last summand.

    lemma weighted_telescope_succ (z w : ℕ → ℂ) (N : ℕ)
        (hstep : ∀ i ≤ N, (z (i + 1) - z i) * w i = z i) :
        (∑ i ∈ Finset.range (N + 1), z i) = z (N + 1) * w N - z 0 * w 0 +
          ∑ i ∈ Finset.range N, z (i + 1) * (w i - w (i + 1)) := by
    …

14. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound line 147

    Source documentation

    A discrete first-derivative estimate (Kusmin--Landau): monotone consecutive phase increments, uniformly separated from the integers, force cancellation. The last increment is included to make the endpoint formula uniform, including N=0.

    theorem first_derivative_sum_bound (f : ℕ → ℝ) (N : ℕ) (β : ℝ) (hβ : 0 < β)
        (hlo : ∀ i ≤ N, β ≤ f (i + 1) - f i)
        (hhi : ∀ i ≤ N, f (i + 1) - f i ≤ 1 - β)
        (hmono : MonotoneOn (fun i => f (i + 1) - f i) (Set.Iic N)) :
        ‖∑ i ∈ Finset.range N, phase (f i)‖ ≤ 2 / β := by
    …

    Mentions: OAI.Problem337.ExponentialSum.phase

15. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound_succ line 204

    Source documentation

    Cancellation using only the increments attached to the summands.

    theorem first_derivative_sum_bound_succ (f : ℕ → ℝ) (N : ℕ) (β : ℝ) (hβ : 0 < β)
        (hlo : ∀ i ≤ N, β ≤ f (i + 1) - f i)
        (hhi : ∀ i ≤ N, f (i + 1) - f i ≤ 1 - β)
        (hmono : MonotoneOn (fun i => f (i + 1) - f i) (Set.Iic N)) :
        ‖∑ i ∈ Finset.range (N + 1), phase (f i)‖ ≤ 2 / β := by
    …

    Mentions: OAI.Problem337.ExponentialSum.phase

16. lemma OAI.Problem337.ExponentialSum.phase_int line 260
17. lemma OAI.Problem337.ExponentialSum.phase_neg line 266
18. lemma OAI.Problem337.ExponentialSum.phase_sub_int_mul line 274
19. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound_strip line 282

    Source documentation

    Integer translations of the increment strip do not affect the estimate.

    theorem first_derivative_sum_bound_strip (f : ℕ → ℝ) (N : ℕ) (β : ℝ) (q : ℤ)
        (hβ : 0 < β)
        (hlo : ∀ i ≤ N, (q : ℝ) + β ≤ f (i + 1) - f i)
        (hhi : ∀ i ≤ N, f (i + 1) - f i ≤ (q : ℝ) + 1 - β)
        (hmono : MonotoneOn (fun i => f (i + 1) - f i) (Set.Iic N)) :
        ‖∑ i ∈ Finset.range N, phase (f i)‖ ≤ 2 / β := by
    …

    Mentions: OAI.Problem337.ExponentialSum.phase

20. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound_either line 306

    Source documentation

    Both directions of monotonicity are allowed in the discrete first-derivative estimate.

    theorem first_derivative_sum_bound_either (f : ℕ → ℝ) (N : ℕ) (β : ℝ) (q : ℤ)
        (hβ : 0 < β)
        (hlo : ∀ i ≤ N, (q : ℝ) + β ≤ f (i + 1) - f i)
        (hhi : ∀ i ≤ N, f (i + 1) - f i ≤ (q : ℝ) + 1 - β)
        (hmono : MonotoneOn (fun i => f (i + 1) - f i) (Set.Iic N) ∨
          AntitoneOn (fun i => f (i + 1) - f i) (Set.Iic N)) :
        ‖∑ i ∈ Finset.range N, phase (f i)‖ ≤ 2 / β := by
    …

    Mentions: OAI.Problem337.ExponentialSum.phase

21. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound_strip_succ line 325
22. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound_either_succ line 349

    Source documentation

    Both directions of monotonicity are allowed in the discrete first-derivative estimate.

    theorem first_derivative_sum_bound_either_succ (f : ℕ → ℝ) (N : ℕ) (β : ℝ) (q : ℤ)
        (hβ : 0 < β)
        (hlo : ∀ i ≤ N, (q : ℝ) + β ≤ f (i + 1) - f i)
        (hhi : ∀ i ≤ N, f (i + 1) - f i ≤ (q : ℝ) + 1 - β)
        (hmono : MonotoneOn (fun i => f (i + 1) - f i) (Set.Iic N) ∨
          AntitoneOn (fun i => f (i + 1) - f i) (Set.Iic N)) :
        ‖∑ i ∈ Finset.range (N + 1), phase (f i)‖ ≤ 2 / β := by
    …

    Mentions: OAI.Problem337.ExponentialSum.phase

23. theorem OAI.Problem337.ExponentialSum.first_derivative_sum_bound_Icc line 369

    Source documentation

    The first-derivative bound on a contiguous block of natural indices.

    theorem first_derivative_sum_bound_Icc (f : ℕ → ℝ) (a b : ℕ) (β : ℝ) (q : ℤ)
        (hβ : 0 < β)
        (hlo : ∀ i, a ≤ i → i ≤ b → (q : ℝ) + β ≤ f (i + 1) - f i)
        (hhi : ∀ i, a ≤ i → i ≤ b → f (i + 1) - f i ≤ (q : ℝ) + 1 - β)
        (hmono : MonotoneOn (fun i => f (i + 1) - f i) (Set.Icc a b) ∨
          AntitoneOn (fun i => f (i + 1) - f i) (Set.Icc a b)) :
        ‖∑ i ∈ Finset.Icc a b, phase (f i)‖ ≤ 2 / β := by
    …

    Mentions: OAI.Problem337.ExponentialSum.phase