RS.SumDiff.variation_le_of_forall_sumAbsDiff_le

Sum of absolute increments of g over an untagged partition. -/ def sumAbsDiff {a b : ℝ} (g : ℝ → ℝ) (P : IPart.IPartition a b) : ℝ := ∑ i : Fin P.n, |g (P.x i.succ) - g (P.x i.castSucc)|

/- The absolute difference of g over a subinterval of P is bounded by the sum of absolute differences of g over the corresponding subintervals of R. -/ lemma sumAbsDiff_block_le {a b : ℝ} {g : ℝ → ℝ} {P R : IPart.IPartition a b} (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk : Monotone k) (hk_eq : ∀ i, R.x (k i) = P.x i) (i : Fin P.n) : |g (P.x i.succ) - g (P.x i.castSucc)| ≤ ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R j| := by rw [← hk_eq i.succ, ← hk_eq i.castSucc] rw [← IPart.sum_telescope_block g R (k i.castSucc) (k i.succ) (hk (Nat.le_succ _))] apply Finset.abs_sum_le_sum_abs

/- sumAbsDiff is monotonic with respect to partition refinement. -/ lemma sumAbsDiff_mono_of_refinement {a b : ℝ} {g : ℝ → ℝ} {P R : IPart.IPartition a b} (hPR : IPart.IsRefinement R P) : sumAbsDiff g P ≤ sumAbsDiff g R := by -- Use refinement_index_map to get k. obtain ⟨k, , hk_eq⟩ : ∃ k : Fin (P.n + 1) → Fin (R.n + 1), Monotone k ∧ ∀ i, R.x (k i) = P.x i := by exact IPart.refinement_index_map P R hPR; -- Apply sumAbsDiff_block_le to bound the sum over P by the double sum over blocks of R. have h_sum_le_double_sum : ∑ i : Fin P.n, |g (P.x i.succ) - g (P.x i.castSucc)| ≤ ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R j| := by exact Finset.sum_le_sum fun i _ => sumAbsDiff_block_le k ‹› ‹_› i; -- Use sum_partition_blocks to collapse the double sum into a single sum over Ico (k 0) (k P.n). have h_double_sum_to_single_sum : ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R j| = ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last P.n)).val, |IPart.term g R j| := by have h_double_sum_to_single_sum : ∀ (n : ℕ) (k : Fin (n + 1) → ℕ) (hk : Monotone k), ∑ i : Fin n, ∑ j ∈ Finset.Ico (k i.castSucc) (k i.succ), |IPart.term g R j| = ∑ j ∈ Finset.Ico (k 0) (k (Fin.last n)), |IPart.term g R j| := by exact fun n k hk ↦ IPart.sum_partition_blocks n k hk fun j ↦ |IPart.term g R j|; convert h_double_sum_to_single_sum P.n ( fun i => ( k i : ℕ ) ) ( fun i j hij => by simpa using ‹Monotone k› hij ) using 1; -- Bound this sum by the sum over range R.n (since terms are non-negative and the interval is a subset). have h_single_sum_le_range : ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last P.n)).val, |IPart.term g R j| ≤ ∑ j ∈ Finset.Ico 0 R.n, |IPart.term g R j| := by refine' Finset.sum_le_sum_of_subset_of_nonneg _ fun _ _ _ => abs_nonneg _; refine' Finset.Ico_subset_Ico _ _ <;> norm_num; exact Nat.le_of_lt_succ ( Fin.is_lt _ ); convert h_sum_le_double_sum.trans ( h_double_sum_to_single_sum.le.trans h_single_sum_le_range ) using 1; simp +decide [ sumAbsDiff, Finset.sum_range, Fin.cast_val_eq_self ]; refine' Finset.sum_congr rfl fun i hi => _ ; unfold IPart.term ; aesop

/- sumAbsDiff is monotonic with respect to partition refinement. -/ lemma sumAbsDiff_le_sumAbsDiff_of_refinement {a b : ℝ} {g : ℝ → ℝ} {P R : IPart.IPartition a b} (hPR : IPart.IsRefinement R P) : sumAbsDiff g P ≤ sumAbsDiff g R := by convert sumAbsDiff_mono_of_refinement hPR using 1

/- If x is a monotone sequence of points contained in partition P, then the sum of absolute differences of g along x is bounded by sumAbsDiff g P. -/ lemma sum_le_sumAbsDiff_of_points_subset {a b : ℝ} (g : ℝ → ℝ) (P : RS.IPart.IPartition a b) (p : ℕ) (x : Fin (p + 1) → ℝ) (hx : Monotone x) (h_subset : ∀ i, x i ∈ P.points) : ∑ i : Fin p, |g (x i.succ) - g (x i.castSucc)| ≤ RS.SumDiff.sumAbsDiff g P := by -- By definition of $P.points$, there exists a monotone map $k : Fin (p + 1) → Fin (P.n + 1)$ such that $P.x (k i) = x i$ for all $i$. obtain ⟨k, hk⟩ : ∃ k : Fin (p + 1) → Fin (P.n + 1), Monotone k ∧ ∀ i : Fin (p + 1), P.x (k i) = x i := by -- By definition of $P.points$, there exists a monotone map $k : Fin (p + 1) → Fin (P.n + 1)$ such that $P.x (k i) = x i$ for all $i$ by the properties of the points of $P$. have h_k_exists : ∀ y ∈ P.points, ∃ i : Fin (P.n + 1), P.x i = y := by exact fun y hy => by rw [ IPart.IPartition.points ] at hy; aesop; choose k hk using h_k_exists; use fun i => k ( x i ) ( h_subset i ); have h_k_mono : ∀ i j : Fin (p + 1), x i ≤ x j → k (x i) (h_subset i) ≤ k (x j) (h_subset j) := by intros i j hij have h_k_mono : P.x (k (x i) (h_subset i)) ≤ P.x (k (x j) (h_subset j)) := by aesop; contrapose! h_k_mono; apply_rules [ P.monotone, lt_of_le_of_ne ]; · exact le_of_lt h_k_mono; · grind; exact ⟨ fun i j hij => h_k_mono i j <| hx hij, fun i => hk _ _ ⟩; -- Apply the lemma sum_telescope_abs_le to each term in the sum. have h_telescope : ∀ i : Fin p, |g (x (i.succ)) - g (x (i.castSucc))| ≤ ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| := by intros i have h_telescope : |g (P.x (k (i.succ))) - g (P.x (k (i.castSucc)))| ≤ ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| := by convert IPart.sum_telescope_abs_le g P ( k ( Fin.castSucc i ) ) ( k ( Fin.succ i ) ) _ using 1; exact hk.1 ( Nat.le_succ _ ); aesop; -- Apply the lemma sum_partition_blocks to combine the sums over the intervals [k i, k (i+1)). have h_sum_partition_blocks : ∑ i : Fin p, ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| ≤ ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last p)).val, |RS.IPart.term g P j| := by have h_sum_partition_blocks : ∑ i : Fin p, ∑ j ∈ Finset.Ico (k (i.castSucc)).val (k (i.succ)).val, |RS.IPart.term g P j| = ∑ j ∈ Finset.Ico (k 0).val (k (Fin.last p)).val, |RS.IPart.term g P j| := by convert RS.IPart.sum_partition_blocks p ( fun i => ( k i : ℕ ) ) hk.1 _ using 1; grind; refine le_trans ( Finset.sum_le_sum fun i _ => h_telescope i ) ( h_sum_partition_blocks.trans ?_ ); refine' le_trans ( Finset.sum_le_sum_of_subset_of_nonneg ( Finset.subset_iff.mpr _ ) fun _ _ _ => abs_nonneg _ ) _; exact Finset.range P.n; · simp +zetaDelta at *; intro i hi₁ hi₂; exact lt_of_lt_of_le hi₂ ( Nat.le_of_lt_succ <| by simp [ Fin.is_lt ] ) ; · simp +decide [ Finset.sum_range, IPart.term ]; rfl

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

/- If the sum of absolute differences of g over any partition is bounded by K, then the total variation of g is bounded by K.