RS.Integ.RSSum_P_rewrite

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.