RS.Integ.mvt_tags_for_partition

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. -/ lemma variation_le_of_forall_sumAbsDiff_le {a b : ℝ} (hab : a < b) (g : ℝ → ℝ) (K : ℝ) (hK : ∀ P : IPart.IPartition a b, sumAbsDiff g P ≤ K) : (eVariationOn g (Set.Icc a b)).toReal ≤ K := by -- We know that for any monotone sequence x, the sum of absolute differences is ≤ K. have h_sum_le : ∀ (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 intro p x hx hx_mem exact sum_le_K_of_forall_sumAbsDiff_le hab g K hK p x hx hx_mem

-- Now we relate this to eVariationOn. -- eVariationOn is the supremum of these sums (converted to ENNReal). -- We show eVariationOn ≤ ENNReal.ofReal K. have h_var_le : eVariationOn g (Set.Icc a b) ≤ ENNReal.ofReal K := by -- Unfold eVariationOn to its definition as a supremum -- Since eVariationOn is defined as a supr, we use iSup_le -- Note: The definition might be wrapped. -- We can try to use eVariationOn properties or just unfold it. -- Assuming standard definition: -- ref: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Variation.html#eVariationOn -- It is iSup over p, x. refine' iSup_le _; rintro ⟨ p, ⟨ x, hx₁, hx₂ ⟩ ⟩; simp_all +decide [ edist_dist, Real.dist_eq ]; convert ENNReal.ofReal_le_ofReal ( h_sum_le p ( fun i => x i ) ( fun i j hij => hx₁ hij ) ( fun i => hx₂ i ) ) using 1; rw [ ENNReal.ofReal_sum_of_nonneg fun _ _ => abs_nonneg _, Finset.sum_range ]; exact rfl

/- If the sum of absolute differences of g over any partition is bounded by K, then the sum of absolute differences along any monotone sequence in [a, b] is bounded by K. -/

-- Finally, convert to Real. apply ENNReal.toReal_le_of_le_ofReal · -- K ≥ 0 have P := RS.IPart.uniformPartition 1 hab have := hK P calc 0 ≤ RS.SumDiff.sumAbsDiff g P := by apply Finset.sum_nonneg intro i _ apply abs_nonneg _ ≤ K := this · exact h_var_le

end SumDiff

/- First, a definition of tagged partitions, followed by some basic lemmas -/ /- A tagged Riemann-Stieltjes partition includes points xi in each subinterval [x_i, x_{i+1}]. -/

namespace Integ

structure TaggedPartition (a b : ℝ) extends IPart.IPartition a b where xi : Fin n → ℝ h_xi : ∀ i : Fin n, x i.castSucc ≤ xi i ∧ xi i ≤ x i.succ

/- The filter of tagged partitions with mesh tending to 0. -/ def TaggedPartitionFilter (a b : ℝ) : Filter (TaggedPartition a b) := Filter.comap (fun P => P.mesh) (nhds 0)

/- A uniform partition with left tags. We need that simply because our filter is a filter of tagged partitions. -/ def taggedUniformPartition {a b : ℝ} (n : ℕ) (hab : a < b) : TaggedPartition a b := let P := IPart.uniformPartition n hab { toIPartition := P xi := fun i => P.x i.castSucc h_xi := by intro i constructor · exact le_refl _ · apply P.monotone apply Nat.le_succ }

/- The partition filter is proper, that is, there exist partitions of [a,b] of arbitrarily small mesh. -/ lemma TaggedPartitionFilter_neBot {a b : ℝ} (hab : a < b) : Filter.NeBot (TaggedPartitionFilter a b) := by refine' Filter.neBot_iff.mpr _; rw [ Ne.eq_def, Filter.ext_iff ]; simp +zetaDelta at *; use ∅; intro h; obtain ⟨ U, hU₁, hU₂ ⟩ := Filter.mem_comap.mp h; simp_all +decide [ Set.subset_def ]; contrapose! hU₂; rcases Metric.mem_nhds_iff.mp hU₁ with ⟨ ε, εpos, hε ⟩; -- Choose $n$ such that $(b - a) / (n + 1) < \epsilon$. obtain ⟨ n, hn ⟩ : ∃ n : ℕ, (b - a) / (n + 1) < ε := by exact ⟨ ⌊ ( b - a ) / ε⌋₊, by rw [ div_lt_iff₀ ] <;> nlinarith [ Nat.lt_floor_add_one ( ( b - a ) / ε ), mul_div_cancel₀ ( b - a ) εpos.ne' ] ⟩; refine' ⟨ taggedUniformPartition n hab, hε _ ⟩; simp +zetaDelta at *; rw [ abs_of_nonneg ( IPart.mesh_nonneg _ ) ]; convert hn using 1; convert IPart.mesh_uniformPartition n hab using 1

/- A tagged partition where the tags are the left endpoints of the intervals. -/ def tagLeft {a b : ℝ} (P : IPart.IPartition a b) : TaggedPartition a b := { P with xi := fun i => P.x i.castSucc h_xi := fun i => ⟨le_refl _, P.monotone (Nat.le_succ _)⟩ }

/- We finally come to Riemann-Stieltjes sums and to the definition of Riemann-Stieltjes integrals!-/ /- The Riemann-Stieltjes sum S(P, f, g) is the sum of f(xi_i) * (g(x_{i+1}) - g(x_i)). -/ def RSSum {a b : ℝ} (f g : ℝ → ℝ) (P : TaggedPartition a b) : ℝ := ∑ i : Fin P.n, f (P.xi i) * (g (P.x i.succ) - g (P.x i.castSucc))

/- The Riemann-Stieltjes integral of f with respect to g on [a, b] has value I. -/ def HasRSIntegral (f g : ℝ → ℝ) (a b I : ℝ) : Prop := ∀ ε > 0, ∃ δ > 0, ∀ (P : TaggedPartition a b), P.mesh ≤ δ → |RSSum f g P - I| < ε

/- HasRSIntegral is equivalent to convergence along the tagged partition filter. -/ lemma hasRSIntegral_iff_tendsto {f g : ℝ → ℝ} {a b I : ℝ} : HasRSIntegral f g a b I ↔ Filter.Tendsto (RSSum f g) (TaggedPartitionFilter a b) (nhds I) := by constructor <;> intro h; · refine' Metric.tendsto_nhds.mpr _; intro ε hε; obtain ⟨ δ, hδ, H ⟩ := h ε hε; filter_upwards [ Filter.preimage_mem_comap ( Iio_mem_nhds hδ ) ] with P hP using H P <| le_of_lt hP; · intro ε hε; obtain ⟨ δ, hδ ⟩ := Metric.tendsto_nhds.mp h ε hε; -- Since δ is a neighborhood of 0, there exists a δ' > 0 such that (0, δ') is contained in δ. obtain ⟨δ', hδ'⟩ : ∃ δ' > 0, Metric.ball 0 δ' ⊆ δ := by exact Metric.mem_nhds_iff.mp hδ.1; use δ' / 2; exact ⟨ half_pos hδ'.1, fun P hP => hδ.2 <| hδ'.2 <| mem_ball_zero_iff.mpr <| abs_lt.mpr ⟨ by linarith [ show 0 ≤ P.mesh from IPart.mesh_nonneg _ ], by linarith [ show 0 ≤ P.mesh from IPart.mesh_nonneg _ ] ⟩ ⟩

/- The Cauchy condition for Riemann-Stieltjes sums. -/ def RSCauchyCondition (f g : ℝ → ℝ) (a b : ℝ) : Prop := ∀ ε > 0, ∃ δ > 0, ∀ (P Q : TaggedPartition a b), P.mesh ≤ δ → Q.mesh ≤ δ → |RSSum f g P - RSSum f g Q| < ε

/- The image of the partition filter under the Riemann sum map is a Cauchy filter. -/ lemma cauchy_map_RSSum {f g : ℝ → ℝ} {a b : ℝ} (hab : a < b) (h : RSCauchyCondition f g a b) : Cauchy (Filter.map (RSSum f g) (TaggedPartitionFilter a b)) := by have h_cauchy : ∀ ε > 0, ∃ S ∈ TaggedPartitionFilter a b, ∀ P Q : TaggedPartition a b, P ∈ S → Q ∈ S → |RSSum f g P - RSSum f g Q| < ε := by intro ε hε_pos obtain ⟨δ, hδ_pos, hδ⟩ := h ε hε_pos use {P : TaggedPartition a b | P.mesh ≤ δ}; exact ⟨ Filter.mem_comap.mpr ⟨ Set.Iic δ, Iic_mem_nhds hδ_pos, by aesop ⟩, hδ ⟩; rw [ Metric.cauchy_iff ]; constructor; · apply_rules [ Filter.map_neBot ]; exact TaggedPartitionFilter_neBot hab; · exact fun ε ε_pos => by obtain ⟨ S, hS₁, hS₂ ⟩ := h_cauchy ε ε_pos; exact ⟨ RSSum f g '' S, Filter.image_mem_map hS₁, by aesop ⟩ ;

/- The Cauchy condition implies the existence of the Riemann-Stieltjes integral. -/ theorem RSCauchy_implies_exists (f g : ℝ → ℝ) (a b : ℝ) (hab : a < b) (h : RSCauchyCondition f g a b) : ∃ I, HasRSIntegral f g a b I := by -- By cauchy_map_RSSum, the filter map (RSSum f g) (TaggedPartitionFilter a b) is Cauchy. have h_cauchy : Cauchy (Filter.map (RSSum f g) (TaggedPartitionFilter a b)) := by exact cauchy_map_RSSum hab h -- Since ℝ is a complete metric space, every Cauchy filter converges. obtain ⟨I, hI⟩ : ∃ I : ℝ, Filter.Tendsto (RSSum f g) (TaggedPartitionFilter a b) (nhds I) := by exact CompleteSpace.complete h_cauchy exact ⟨ I, by simpa only [ hasRSIntegral_iff_tendsto ] using hI ⟩

/- Rewrite S(P) as a double sum using the refinement index map. -/ lemma RSSum_P_rewrite {a b : ℝ} (f g : ℝ → ℝ) (P R : TaggedPartition a b) (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk : Monotone k) (hk_eq : ∀ i, R.x (k i) = P.x i) : RSSum f g P = ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, f (P.xi i) * IPart.term g R.toIPartition j := by apply Finset.sum_congr rfl fun i _ => ?_; have h_telescope : ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, IPart.term g R.toIPartition j = g (R.x (k i.succ)) - g (R.x (k i.castSucc)) := by convert IPart.sum_telescope_block g R.toIPartition ( k i.castSucc ) ( k i.succ ) ( hk ( Nat.le_succ _ ) ) using 1; simp_all +decide [ ← Finset.mul_sum _ _ _, ← Finset.sum_mul ]

/- Term in Riemann sum of R at index j. -/ def term_f_g {a b : ℝ} (f g : ℝ → ℝ) (R : TaggedPartition a b) (j : ℕ) : ℝ := if h : j < R.n then f (R.xi ⟨j, h⟩) * IPart.term g R.toIPartition j else 0

/- Rewrite the Riemann sum of R as a double sum over blocks defined by P, using the index map k. -/ lemma RSSum_R_rewrite {a b : ℝ} (f g : ℝ → ℝ) (P R : TaggedPartition a b) (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk : Monotone k) (hk_0 : k 0 = 0) (hk_eq : ∀ i, R.x (k i) = P.x i) : RSSum f g R = ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, term_f_g f g R j := by have h_rewrite : ∑ j ∈ Finset.range R.n, term_f_g f g R j = ∑ j ∈ Finset.Ico 0 (k (Fin.last P.n)).val, term_f_g f g R j := by -- Since $R.x m = b$ and $R.x$ is monotone, for $j \geq m$, $R.x j = b$. have h_monotone : ∀ j : Fin (R.n + 1), (k (Fin.last P.n)).val ≤ j.val → R.x j = b := by intros j hj have h_monotone : ∀ i j : Fin (R.n + 1), i ≤ j → R.x i ≤ R.x j := by exact R.monotone; have h_monotone : R.x (k (Fin.last P.n)) = b := by exact hk_eq _ ▸ P.right; exact le_antisymm ( by linarith [ R.monotone ( show j ≤ Fin.last _ from Fin.le_last _ ), R.right ] ) ( by linarith [ ‹∀ i j : Fin ( R.n + 1 ), i ≤ j → R.x i ≤ R.x j› _ _ ( show k ( Fin.last P.n ) ≤ j from hj ) ] ); -- Since $R.x j = b$ for $j \geq m$, the term_f_g $f$ $g$ $R$ $j$ is zero for $j \geq m$. have h_zero : ∀ j : ℕ, (k (Fin.last P.n)).val ≤ j → j < R.n → term_f_g f g R j = 0 := by intros j hj₁ hj₂ have h_x_eq_b : R.x ⟨j + 1, by linarith⟩ = b := by exact h_monotone _ ( Nat.le_succ_of_le hj₁ ); have h_x_eq_b : R.x ⟨j, by linarith⟩ = b := by exact h_monotone ⟨ j, by linarith ⟩ hj₁; unfold term_f_g IPart.term; aesop; rw [ ← Finset.sum_range_add_sum_Ico _ ( show ( k ( Fin.last P.n ) |> Fin.val ) ≤ R.n from Nat.le_of_lt_succ <| Fin.is_lt _ ) ]; simp +zetaDelta at *; exact Finset.sum_eq_zero fun x hx => h_zero x ( Finset.mem_Ico.mp hx |>.1 ) ( Finset.mem_Ico.mp hx |>.2 ); convert h_rewrite using 1; · unfold RSSum term_f_g; unfold IPart.term; simp +decide [ Finset.sum_range, Fin.sum_univ_castSucc ] ; rfl; · convert IPart.sum_partition_blocks P.n ( fun i => ( k i : ℕ ) ) ( fun i j hij => by simpa using hk hij ) ( fun j => term_f_g f g R j ) using 1; aesop

/- Now we start proving meaningful bounds.-/

/- The sum of absolute differences of g over a partition is bounded by the total variation of g. -/ lemma sum_abs_diff_le_variation {g : ℝ → ℝ} {a b : ℝ} (P : IPart.IPartition a b) (hg : BoundedVariationOn g (Set.Icc a b)) : ∑ i : Fin P.n, |g (P.x i.succ) - g (P.x i.castSucc)| ≤ (eVariationOn g (Set.Icc a b)).toReal := by have h_sum_le_eVariationOn : ∑ i : Fin P.n, ENNReal.ofReal (abs ((g (P.x i.succ)) - (g (P.x i.castSucc)))) ≤ eVariationOn g (Set.Icc a b) := by refine' le_trans _ ( eVariationOn.mono g _ ); swap; exact Set.range P.x; · refine' le_trans _ ( le_ciSup _ ⟨ P.n, _ ⟩ ); rotate_right; use fun i => if hi : i ≤ P.n then P.x ⟨ i, by linarith ⟩ else P.x ⟨ P.n, by linarith ⟩; refine' ⟨ _, _ ⟩; intro i j hij; all_goals norm_num [ edist_dist ]; · split_ifs <;> try linarith [ P.monotone ( show ⟨ i, by linarith ⟩ ≤ ⟨ j, by linarith ⟩ from Nat.le_trans hij ( Nat.le_refl _ ) ) ]; · exact P.monotone ( Nat.le_trans ( Nat.le_of_lt_succ ( by linarith ) ) ( Nat.le_refl _ ) ); · norm_num; · aesop; · rw [ Finset.sum_range ]; refine' Finset.sum_le_sum fun i _ => _; split_ifs <;> norm_num [ Nat.succ_le_iff ]; · rfl; · linarith [ Fin.is_lt i ]; · exact False.elim <| ‹¬ ( i : ℕ ) + 1 ≤ P.n› <| Nat.succ_le_of_lt <| Fin.is_lt i; · linarith [ Fin.is_lt i ]; · rintro _ ⟨ i, rfl ⟩ ; exact ⟨ by linarith [ P.monotone ( show 0 ≤ i from Nat.zero_le _ ), P.left ], by linarith [ P.monotone ( show i ≤ Fin.last P.n from Fin.le_last _ ), P.right ] ⟩ ; convert ENNReal.toReal_mono _ h_sum_le_eVariationOn using 1; · rw [ ENNReal.toReal_sum ] ; aesop; exact fun _ _ => ENNReal.ofReal_ne_top; · exact hg

/- For a fixed interval of the coarser partition, the sum of the weighted differences is bounded by epsilon times the sum of the absolute differences of g. -/ lemma inner_sum_bound {f g : ℝ → ℝ} {a b : ℝ} (P R : TaggedPartition a b) (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk : Monotone k) (hk_eq : ∀ i, R.x (k i) = P.x i) (ε : ℝ) (hε : 0 ≤ ε) (h_osc : ∀ i : Fin P.n, ∀ x ∈ Set.Icc (P.x i.castSucc) (P.x i.succ), |f (P.xi i) - f x| ≤ ε) (i : Fin P.n) : ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, (if h : j < R.n then |(f (P.xi i) - f (R.xi ⟨j, h⟩)) * IPart.term g R.toIPartition j| else 0) ≤ ε * ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, |IPart.term g R.toIPartition j| := by rw [ Finset.mul_sum _ _ _ ]; refine' Finset.sum_le_sum fun j hj => _; split_ifs <;> simp_all +decide [ abs_mul ]; · refine' mul_le_mul_of_nonneg_right ( h_osc i _ _ _ ) ( abs_nonneg _ ); · have := R.h_xi ⟨ j, by linarith ⟩; exact le_trans ( hk_eq _ ▸ R.monotone ( show k i.castSucc ≤ ⟨ j, by linarith ⟩ from hj.1 ) ) this.1; · have := R.h_xi ⟨ j, by linarith ⟩; exact le_trans this.2 ( hk_eq ( Fin.succ i ) ▸ R.monotone ( Nat.le_of_lt_succ ( by aesop ) ) ); · positivity

/- The difference between the Riemann sums of a partition and its refinement is bounded by ε times the total variation of g, provided the oscillation of f on the coarser partition is bounded by ε. -/ lemma RSSum_diff_bound {f g : ℝ → ℝ} {a b : ℝ} (P R : TaggedPartition a b) (k : Fin (P.n + 1) → Fin (R.n + 1)) (hk : Monotone k) (hk_eq : ∀ i, R.x (k i) = P.x i) (hk_0 : k 0 = 0) (ε : ℝ) (hε : 0 ≤ ε) (h_osc : ∀ i : Fin P.n, ∀ x ∈ Set.Icc (P.x i.castSucc) (P.x i.succ), |f (P.xi i) - f x| ≤ ε) (hg : BoundedVariationOn g (Set.Icc a b)) : |RSSum f g P - RSSum f g R| ≤ ε * (eVariationOn g (Set.Icc a b)).toReal := by -- Applying the triangle inequality and the bounds from inner_sum_bound, we get: have h_triangle : abs (RSSum f g P - RSSum f g R) ≤ ∑ i : Fin P.n, ε * ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, abs (IPart.term g R.toIPartition j) := by convert Finset.abs_sum_le_sum_abs _ _ |> le_trans <| Finset.sum_le_sum fun i _ => ?_ using 2; any_goals try infer_instance; rw [ RSSum_P_rewrite f g P R k hk hk_eq, RSSum_R_rewrite f g P R k hk hk_0 hk_eq ]; rw [ ← Finset.sum_sub_distrib ]; rw [ Finset.mul_sum _ _ _ ]; convert Finset.abs_sum_le_sum_abs _ _ |> le_trans <| Finset.sum_le_sum fun j hj => ?_ using 2; rw [ ← Finset.sum_sub_distrib ]; · infer_instance; · infer_instance; · unfold term_f_g; split_ifs <;> simp_all +decide [ abs_mul ]; · rw [ ← sub_mul ]; rw [ abs_mul ]; gcongr; apply h_osc i (R.xi ⟨j, by linarith⟩); · have := R.h_xi ⟨ j, by linarith ⟩; exact le_trans ( hk_eq _ ▸ R.monotone ( Nat.le_trans ( Nat.le_of_lt_succ ( by aesop ) ) hj.1 ) ) this.1; · have := R.h_xi ⟨ j, by linarith ⟩; exact this.2.trans ( hk_eq ( Fin.succ i ) ▸ R.monotone ( Nat.le_of_lt_succ ( by aesop ) ) ); · linarith [ Fin.is_lt ( k i.castSucc ), Fin.is_lt ( k i.succ ) ]; -- Summing over $i$, we get: have h_sum : ∑ i : Fin P.n, ε * ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, abs (IPart.term g R.toIPartition j) ≤ ε * ∑ j ∈ Finset.Ico 0 (k (Fin.last P.n)).val, abs (IPart.term g R.toIPartition j) := by have h_sum : ∑ i : Fin P.n, ∑ j ∈ Finset.Ico (k i.castSucc).val (k i.succ).val, abs (IPart.term g R.toIPartition j) = ∑ j ∈ Finset.Ico 0 (k (Fin.last P.n)).val, abs (IPart.term g R.toIPartition j) := by convert IPart.sum_partition_blocks P.n ( fun i => ( k i : ℕ ) ) ( fun i j hij => hk hij ) ( fun j => |IPart.term g R.toIPartition j| ) using 1; aesop; rw [ ← h_sum, Finset.mul_sum _ _ _ ]; -- Since $k (Fin.last P.n) \leq R.n$, we have: have h_last : ∑ j ∈ Finset.Ico 0 (k (Fin.last P.n)).val, abs (IPart.term g R.toIPartition j) ≤ ∑ j ∈ Finset.range R.n, abs (IPart.term g R.toIPartition j) := by exact Finset.sum_le_sum_of_subset_of_nonneg ( fun x hx => Finset.mem_range.mpr ( by linarith [ Finset.mem_Ico.mp hx, Fin.is_lt ( k ( Fin.last P.n ) ) ] ) ) fun _ _ _ => abs_nonneg ; refine le_trans h_triangle <| h_sum.trans <| mul_le_mul_of_nonneg_left ( h_last.trans ? ) hε; convert sum_abs_diff_le_variation R.toIPartition hg using 1; simp +decide [ Finset.sum_range, IPart.term ]; rfl

/- If the mesh of a partition is small enough such that any two points within distance mesh satisfy the uniform continuity condition, then the oscillation of f on each subinterval is bounded. -/ lemma oscillation_bound_of_mesh {f : ℝ → ℝ} {a b : ℝ} {ε δ : ℝ} (P : TaggedPartition a b) (h_mesh : P.mesh ≤ δ) (h_unif : ∀ x y, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |x - y| ≤ δ → |f x - f y| ≤ ε) : ∀ i : Fin P.n, ∀ x ∈ Set.Icc (P.x i.castSucc) (P.x i.succ), |f (P.xi i) - f x| ≤ ε := by intros i x hx have h_dist : |P.xi i - x| ≤ P.mesh := by -- By definition of mesh, we know that for any $i$, $|P.x i - P.x (i + 1)| \leq P.mesh$. have h_mesh_le : ∀ i : Fin P.n, |P.x (i.castSucc) - P.x (i.succ)| ≤ P.mesh := by intro i have h_diff_le_mesh : ∀ i : Fin P.n, P.x i.succ - P.x i.castSucc ≤ P.mesh := by intro i have h_diff_le_mesh : P.x i.succ - P.x i.castSucc ∈ Finset.image (fun i => P.x i.succ - P.x i.castSucc) (Finset.univ : Finset (Fin P.n)) := by exact Finset.mem_image_of_mem _ ( Finset.mem_univ _ ); have h_diff_le_mesh : ∀ y ∈ Finset.image (fun i => P.x i.succ - P.x i.castSucc) (Finset.univ : Finset (Fin P.n)), y ≤ P.mesh := by intros y hy have h_diff_le_mesh : y ≤ Finset.max (Finset.image (fun i => P.x i.succ - P.x i.castSucc) (Finset.univ : Finset (Fin P.n))) := by exact Finset.le_max hy; rw [ show P.mesh = ( Finset.image ( fun i : Fin P.n => P.x i.succ - P.x i.castSucc ) Finset.univ ).max.getD 0 from ?_ ]; · cases h : Finset.max ( Finset.image ( fun i : Fin P.n => P.x i.succ - P.x i.castSucc ) Finset.univ ) <;> aesop; · exact rfl exact h_diff_le_mesh _ ‹›; rw [ abs_sub_comm, abs_of_nonneg ] <;> linarith [ h_diff_le_mesh i, P.monotone ( show i.castSucc ≤ i.succ from Nat.le_succ _ ) ]; exact abs_le.mpr ⟨ by linarith [ abs_le.mp ( h_mesh_le i ), P.h_xi i, hx.1, hx.2 ], by linarith [ abs_le.mp ( h_mesh_le i ), P.h_xi i, hx.1, hx.2 ] ⟩; apply h_unif _ _ ? ?_ <| h_dist.trans h_mesh; · exact ⟨ by linarith [ P.h_xi i, P.left, P.right, P.monotone ( show 0 ≤ Fin.castSucc i from Nat.zero_le _ ) ], by linarith [ P.h_xi i, P.left, P.right, P.monotone ( show Fin.succ i ≤ Fin.last P.n from Fin.le_last _ ) ] ⟩; · exact ⟨ by linarith [ hx.1, P.monotone ( show 0 ≤ Fin.castSucc i from Nat.zero_le _ ), P.left ], by linarith [ hx.2, P.monotone ( show Fin.succ i ≤ Fin.last P.n from Fin.le_last _ ), P.right ] ⟩

/- If f is continuous and g has bounded variation, the Riemann-Stieltjes sums satisfy the Cauchy condition. -/ lemma RS_cauchy_of_continuous_bv {f g : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (hg : BoundedVariationOn g (Set.Icc a b)) : RSCauchyCondition f g a b := by intro ε hε let V := (eVariationOn g (Set.Icc a b)).toReal let ε' := ε / (3 * (V + 1)); -- Choose δ such that |x - y| ≤ δ implies |f x - f y| ≤ ε'. obtain ⟨δ, hδ_pos, hδ⟩ : ∃ δ > 0, ∀ x y : ℝ, x ∈ Set.Icc a b → y ∈ Set.Icc a b → |x - y| ≤ δ → |f x - f y| ≤ ε' := by have := Metric.uniformContinuousOn_iff.mp ( isCompact_Icc.uniformContinuousOn_of_continuous hf ) ε' ( by exact div_pos hε ( by linarith [ show 0 ≤ V by exact ENNReal.toReal_nonneg ] ) ); exact ⟨ this.choose / 2, half_pos this.choose_spec.1, fun x y hx hy hxy => le_of_lt ( this.choose_spec.2 x hx y hy ( by rw [ Real.dist_eq ] ; exact lt_of_le_of_lt hxy ( half_lt_self this.choose_spec.1 ) ) ) ⟩; refine' ⟨ δ, hδ_pos, fun P Q hP hQ => _ ⟩; -- Let R_untagged = IPart.union P.toIPart.IPartition Q.toIPart.IPartition. set R_untagged := IPart.union P.toIPartition Q.toIPartition; -- Apply RSSum_diff_bound to (P, R) and (Q, R) to get |S(P) - S(R)| ≤ ε' * V and |S(Q) - S(R)| ≤ ε' * V. have h_diff_P_R : |RSSum f g P - RSSum f g (tagLeft R_untagged)| ≤ ε' * V := by apply RSSum_diff_bound; exact Classical.choose_spec ( IPart.refinement_index_map P.toIPartition R_untagged ( IPart.union_refines_left P.toIPartition Q.toIPartition ) ) |>.1; · exact Classical.choose_spec ( IPart.refinement_index_map P.toIPartition R_untagged ( IPart.union_refines_left P.toIPartition Q.toIPartition ) ) |>.2; · apply IPart.index_map_zero; · exact IPart.union_strictMono P.toIPartition Q.toIPartition · exact Classical.choose_spec ( IPart.refinement_index_map P.toIPartition R_untagged ( IPart.union_refines_left P.toIPartition Q.toIPartition ) ) |>.2; · exact div_nonneg hε.le ( mul_nonneg zero_le_three ( add_nonneg ( ENNReal.toReal_nonneg ) zero_le_one ) ); · apply oscillation_bound_of_mesh P hP hδ; · assumption have h_diff_Q_R : |RSSum f g Q - RSSum f g (tagLeft R_untagged)| ≤ ε' * V := by apply RSSum_diff_bound; any_goals assumption; case k => exact fun i => ( IPart.refinement_index_map _ _ ( IPart.union_refines_right _ _ ) ) |> Classical.choose |> fun k => k i; · exact Classical.choose_spec ( IPart.refinement_index_map _ _ ( IPart.union_refines_right _ _ ) ) |>.1; · exact Classical.choose_spec ( IPart.refinement_index_map _ _ ( IPart.union_refines_right _ _ ) ) |>.2; · exact IPart.index_map_zero ( IPart.union_strictMono _ _ ) _ ( Classical.choose_spec ( IPart.refinement_index_map _ _ ( IPart.union_refines_right _ _ ) ) |>.2 ); · positivity; · apply oscillation_bound_of_mesh Q hQ hδ; exact abs_lt.mpr ⟨ by nlinarith [ abs_le.mp h_diff_P_R, abs_le.mp h_diff_Q_R, show 0 ≤ ε' by positivity, show 0 ≤ V by exact ENNReal.toReal_nonneg, mul_div_cancel₀ ε ( by linarith [ show 0 ≤ V by exact ENNReal.toReal_nonneg ] : ( 3 * ( V + 1 ) ) ≠ 0 ) ], by nlinarith [ abs_le.mp h_diff_P_R, abs_le.mp h_diff_Q_R, show 0 ≤ ε' by positivity, show 0 ≤ V by exact ENNReal.toReal_nonneg, mul_div_cancel₀ ε ( by linarith [ show 0 ≤ V by exact ENNReal.toReal_nonneg ] : ( 3 * ( V + 1 ) ) ≠ 0 ) ] ⟩

/- Auxiliary definitions for the swapped partition points and tags. -/ def swap_x {a b : ℝ} (P : TaggedPartition a b) : Fin (P.n + 2) → ℝ := Fin.cons a (Fin.snoc P.xi b)

def swap_xi {a b : ℝ} (P : TaggedPartition a b) : Fin (P.n + 1) → ℝ := P.x

/- Given a tagged partition P, construct a 'swapped' partition Q where the points of Q are the tags of P (interleaved with endpoints) and the tags of Q are the points of P. -/ def swapTaggedPartition {a b : ℝ} (P : TaggedPartition a b) : TaggedPartition a b := { n := P.n + 1 x := swap_x P monotone := by intro i j hij; induction' i using Fin.cases with i ih_i ; induction' j using Fin.cases with j ih_j ; aesop; · unfold swap_x; simp +decide [ Fin.cons, Fin.snoc ]; split_ifs <;> simp_all +decide [ Fin.castSucc_lt_last ]; · have := P.h_xi ( Fin.castLT j ‹› ); linarith [ P.monotone ( show 0 ≤ Fin.castSucc ( Fin.castLT j ‹› ) from Nat.zero_le _ ), P.left ]; · linarith [ P.left, P.right, P.monotone ( show 0 ≤ Fin.last P.n from Nat.zero_le _ ) ]; · induction' j using Fin.inductionOn with j ih_j; · tauto; · cases hij.eq_or_lt <;> simp_all +decide [ swap_x ]; simp +decide [ Fin.snoc, * ]; split_ifs <;> simp_all +decide [ Fin.castLT ]; · -- Since $P$ is a partition, its points are monotone. have h_monotone : Monotone P.x := by exact P.monotone; exact h_monotone ( Nat.succ_le_of_lt ‹› ) |> le_trans ( P.h_xi _ |>.2 ) |> le_trans <| P.h_xi _ |>.1; · exact P.h_xi _ |>.2.trans ( P.monotone ( Fin.le_last _ ) ) |> le_trans <| by linarith [ P.right ] ; · exact absurd ‹› ( not_le_of_gt ( Nat.lt_of_lt_of_le ‹_› ( Nat.le_of_lt_succ ( by linarith [ Fin.is_lt i, Fin.is_lt j ] ) ) ) ) left := by rfl right := by -- By definition of swap_x, the last element of the list is b. simp [swap_x] xi := swap_xi P h_xi := by intro i unfold swap_x swap_xi refine' ⟨ _, _ ⟩; · induction' i using Fin.inductionOn with i IH; · exact P.left.ge; · simp +zetaDelta at *; exact P.h_xi i |>.2; · induction i using Fin.lastCases <;> simp_all +decide [ Fin.cons, Fin.snoc ]; · simp +decide [ Fin.last, Fin.snoc ]; exact P.right.le; · exact P.h_xi _ |>.1 }

/- The Riemann-Stieltjes sum of g with respect to f on P is equal to the boundary terms minus the Riemann-Stieltjes sum of f with respect to g on the swapped partition Q. -/ lemma RSSum_swap_identity {a b : ℝ} {f g : ℝ → ℝ} (P : TaggedPartition a b) : RSSum g f P = f b * g b - f a * g a - RSSum f g (swapTaggedPartition P) := by unfold swapTaggedPartition Integ.RSSum; -- By definition of swap_x and swap_xi, we can expand the sums. have h_expand : ∑ x : Fin (P.n + 1), f (swap_xi P x) * (g (swap_x P x.succ) - g (swap_x P x.castSucc)) = ∑ x : Fin (P.n + 1), f (P.x x) * (g (swap_x P x.succ) - g (swap_x P x.castSucc)) := by rfl; have h_telescope : ∑ x : Fin (P.n + 1), f (P.x x) * g (swap_x P x.succ) = f b * g b + ∑ x : Fin P.n, f (P.x x.castSucc) * g (P.xi x) := by rw [ Fin.sum_univ_castSucc ]; simp +decide [ add_comm, swap_x ]; exact Or.inl ( congr_arg f ( P.right ) ); have h_telescope : ∑ x : Fin (P.n + 1), f (P.x x) * g (swap_x P x.castSucc) = f a * g a + ∑ x : Fin P.n, f (P.x x.succ) * g (P.xi x) := by convert Fin.sum_univ_succ _ using 1; congr! 2; · exact P.left.symm ▸ rfl; · unfold swap_x; aesop; simp_all +decide [ mul_sub, sub_mul, mul_comm, Finset.sum_add_distrib, Finset.mul_sum _ _ _ ] ; ring

/- The length of any interval in the swapped partition is at most twice the mesh of the original partition. -/ lemma swap_diff_le {a b : ℝ} (P : TaggedPartition a b) (j : Fin (P.n + 1)) : (swapTaggedPartition P).x j.succ - (swapTaggedPartition P).x j.castSucc ≤ 2 * P.mesh := by cases j using Fin.inductionOn; · unfold swapTaggedPartition; unfold swap_x; rcases P with ⟨ ⟨ n, x, hx ⟩, xi, hxi ⟩; rcases n with ( _ | n ) <;> norm_num [ Fin.cons ] at *; · simp_all +decide [ Fin.snoc ]; unfold IPart.IPartition.mesh; aesop; · have := hxi 0; norm_num at *; linarith! [ hx ( show 0 ≤ 1 from Nat.zero_le _ ), IPart.mesh_ge_diff ⟨ n + 1, x, hx, by tauto, by tauto ⟩ 0 ] ; · unfold swapTaggedPartition; unfold swap_x; simp +decide [ Fin.cons, Fin.snoc ]; split_ifs <;> simp_all +decide [ Fin.ext_iff ]; · rename_i i hi; have h_diff : P.xi (i.succ.castLT hi) ≤ P.x (i.succ.castLT hi).succ ∧ P.x (i.succ.castLT hi).succ ≤ P.x (i.succ.castLT hi).castSucc + P.mesh := by have h_diff : P.x (i.succ.castLT hi).succ - P.x (i.succ.castLT hi).castSucc ≤ P.mesh := by exact IPart.mesh_ge_diff P.toIPartition (i.succ.castLT hi); exact ⟨ P.h_xi _ |>.2, by linarith ⟩; have h_diff : P.x (i.succ.castLT hi).castSucc - P.x i.castSucc ≤ P.mesh := by have h_diff : ∀ j : Fin P.n, P.x (j.succ) - P.x j.castSucc ≤ P.mesh := by exact fun j ↦ IPart.mesh_ge_diff P.toIPartition j; convert h_diff i using 1; linarith [ P.h_xi i ]; · rename_i i hi; -- Since $P.xi i \leq b$, we have $b - P.xi i \leq b - P.xi i$. have h_le : b - P.xi i ≤ P.mesh := by have h_le : b - P.xi i ≤ P.x (Fin.last P.n) - P.x i.castSucc := by have := P.h_xi i; linarith [ P.right, P.monotone ( show i.castSucc ≤ Fin.last P.n from Fin.le_last _ ), P.monotone ( show i.succ ≤ Fin.last P.n from Fin.le_last _ ) ]; refine le_trans h_le ?_; have h_le : ∀ j : Fin P.n, P.x (Fin.succ j) - P.x (Fin.castSucc j) ≤ P.mesh := by exact fun j ↦ IPart.mesh_ge_diff P.toIPartition j; cases hi.eq_or_lt <;> simp_all +decide [ Fin.eq_last_of_not_lt ]; · convert h_le i using 1; congr ; aesop; · linarith [ Fin.is_lt i ]; linarith [ show 0 ≤ P.mesh from IPart.mesh_nonneg P.toIPartition ]

/- The mesh of the swapped partition is at most twice the mesh of the original partition. -/ lemma mesh_swap_le {a b : ℝ} (P : TaggedPartition a b) : (swapTaggedPartition P).mesh ≤ 2 * P.mesh := by convert Basic.max_getD_le _ _; · exact mul_nonneg zero_le_two ( IPart.mesh_nonneg _ ); · simp +zetaDelta at *; intro i; linarith! [ swap_diff_le P i ] ;

/- Given a partition P and a function g differentiable on [a,b] with derivative g', there exists a tagged partition T with the same points as P such that the increments of g satisfy the Mean Value Theorem equation on each subinterval.