feat(measure_theory/measure/finite_measure_weak_convergence): Charact…

…erize weak convergence of finite measures in terms of integrals of bounded continuous real-valued functions. (#14578)

Weak convergence of measures was defined in terms of integrals of bounded continuous nnreal-valued functions. This PR shows the equivalence to the textbook condition in terms of integrals of bounded continuous real-valued functions.

Also the file `measure_theory/measure/finite_measure_weak_convergence.lean` is divided to sections with dosctrings for clarity.



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/algebra/order/ring.lean

@@ -1225,6 +1225,14 @@ begin
     exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩ }
 end
 
+@[simp] lemma max_zero_add_max_neg_zero_eq_abs_self (a : α) :
+  max a 0 + max (-a) 0 = |a| :=
+begin
+  symmetry,
+  rcases le_total 0 a with ha|ha;
+  simp [ha],
+end
+
 lemma gt_of_mul_lt_mul_neg_left (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
 have nhc : 0 ≤ -c, from neg_nonneg_of_nonpos hc,
 have h2 : -(c * b) < -(c * a), from neg_lt_neg h,