lebesgue differentiation, ftc, lebesgue's density

math-comp · Dec 21, 2023 · b499b5c · b499b5c
1 parent 7d503c9
commit b499b5c
Show file tree

Hide file tree

Showing 4 changed files with 1,426 additions and 9 deletions.
diff --git a/theories/charge.v b/theories/charge.v
@@ -585,7 +585,7 @@ have [v [v0 Pv]] : {v : nat -> elt_type |
     v 0%N = exist _ (A0, d_ set0, A0) (And4 mA0 A0D (d_ge0 set0) A0d0) /\
     forall n, elt_rel (v n) (v n.+1)}.
   apply: dependent_choice_Type => -[[[A' ?] U] [/= mA' A'D]].
-  have [A1 [mA1 A1DU A1t1] ] := next_elt U.
+  have [A1 [mA1 A1DU A1t1]] := next_elt U.
   have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl.
   by exists (exist _ (A1, d_ U, U `|` A1) (And4 mA1 A1D (d_ge0 U) A1t1)).
 have Ubig n : U_ (v n) = \big[setU/set0]_(i < n.+1) A_ (v i).