OAI/NumberTheory/EgyptianFractions/PhaseExtension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.affineTailPhase line 9

   Source documentation

   Extend a finite phase by keeping its final increment constant.

   def affineTailPhase (f : ℕ → ℝ) (N n : ℕ) : ℝ :=
   …

2. theorem OAI.Problem337.affineTailPhase_increment line 13
3. theorem OAI.Problem337.affineTailPhase_eq line 19
4. theorem OAI.Problem337.affineTailPhase_increment_monotone line 32
5. theorem OAI.Problem337.affineTailPhase_increment_antitone line 45
6. theorem OAI.Problem337.affineTailPhase_increment_eq line 58
7. theorem OAI.Problem337.exists_monotone_increment_extension line 64

   Source documentation

   Local interval monotonicity is enough whenever a phase-sum theorem assumes globally monotone increments: this extension preserves every sample used.

   theorem exists_monotone_increment_extension (f : ℕ → ℝ) (N : ℕ) (hN : 0 < N)
       (hmono : MonotoneOn (fun j => f (j + 1) - f j) (Set.Iio N)) :
       ∃ g : ℕ → ℝ, (∀ j, j ≤ N → g j = f j) ∧
         Monotone (fun j => g (j + 1) - g j) ∧
         (∀ j, j < N → g (j + 1) - g j = f (j + 1) - f j) := by
   …

8. theorem OAI.Problem337.exists_antitone_increment_extension line 74

   Source documentation

   The corresponding decreasing-increment extension.

   theorem exists_antitone_increment_extension (f : ℕ → ℝ) (N : ℕ) (hN : 0 < N)
       (hmono : AntitoneOn (fun j => f (j + 1) - f j) (Set.Iio N)) :
       ∃ g : ℕ → ℝ, (∀ j, j ≤ N → g j = f j) ∧
         Antitone (fun j => g (j + 1) - g j) ∧
         (∀ j, j < N → g (j + 1) - g j = f (j + 1) - f j) := by
   …