Source indexedlemma · leanprover/lean4:v4.32.0

RS.SumDiff.sum_le_K_of_forall_sumAbsDiff_le

PrimeNumberTheoremAnd.Unused.MyMV_A3a · PrimeNumberTheoremAnd/Unused/MyMV_A3a.lean:726 to 739

Mathematical statement

Exact Lean statement

lemma sum_le_K_of_forall_sumAbsDiff_le {a b : ℝ} (hab : a < b)
    (g : ℝ → ℝ) (K : ℝ)
    (hK : ∀ P : RS.IPart.IPartition a b, sumAbsDiff g P ≤ K)
    (p : ℕ) (x : Fin (p + 1) → ℝ) (hx : Monotone x) (hx_mem : ∀ i, x i ∈ Set.Icc a b) :
    ∑ i : Fin p, |g (x i.succ) - g (x i.castSucc)| ≤ K

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_le_K_of_forall_sumAbsDiff_le {a b : ℝ} (hab : a < b)    (g : ℝ → ℝ) (K : ℝ)    (hK : ∀ P : RS.IPart.IPartition a b, sumAbsDiff g P ≤ K)    (p : ℕ) (x : Fin (p + 1) → ℝ) (hx : Monotone x) (hx_mem : ∀ i, x i ∈ Set.Icc a b) :    ∑ i : Fin p, |g (x i.succ) - g (x i.castSucc)| ≤ K := by      -- Let `s` be the set of values of `x` union `{a, b}`.      set s : Finset ℝ := Finset.image x Finset.univ ∪ {a, b} with hs_def;      -- Construct a partition `P` from `s` using `RS.IPart.fromPoints`.      obtain ⟨P, hP⟩ : ∃ P : IPart.IPartition a b, P.points = s := by        refine' ⟨ IPart.fromPoints s _ _ _, _ ⟩ <;> norm_num [ hs_def ];        grind;        convert IPart.points_fromPoints _ _ _ _;      convert sum_le_sumAbsDiff_of_points_subset g P p x hx _ |> le_trans <| hK P;      grind