Merge remote-tracking branch 'upstream/master' into LL/small

TestingLowerBounds/ForMathlib/ByParts.lean

@@ -5,16 +5,24 @@ Here there is the statement of a version of the integration by parts theorem for
 This is a generalization of the integration by parts theorem for the Riemann integral. We state it only for the case of Stieltjes functions, that is right continuous and non decreasing, this is because in that case the functions naturally gives rise to a measure. It may be generalized to the more general case with signed measures, but it is necessary to pinpoint the right conditions for that case and it may be necessary to write the definition of the signed measure that arises from a function (I don't know the exact hp for the function, maybe bounded variation?).
 For now I am only stating the theorem and I'm leaving the proof for later.
 Some references for potential candidates for the proof are:
-http://mathonline.wikidot.com/the-formula-for-integration-by-parts-of-riemann-stieltjes-in
-Mathematical analysis, Tom M. Apostol, 5th edition theorem 7.6, page 144 (seems similar to the previous link, in the link it is a bit longer, but maybe it's just that it has more details)
-The integrals of Lebesgue, Denjoy, Perron, and Henstock, theorem 12.14
+http://mathonline.wikidot.com/the-formula-for-integration-by-parts-of-riemann-stieltjes-in [1]
+Mathematical analysis, Tom M. Apostol, 5th edition [2] theorem 7.6, page 144 (seems similar to the previous link, in the link it is a bit longer, but maybe it's just that it has more details)
+The integrals of Lebesgue, Denjoy, Perron, and Henstock [3], theorem 12.14
 
-See also https://math.ryerson.ca/~niushan/Stieltjes-integrals.pdf for some facts about Riemann-Stieltjes and Lebesgue integrals.
+See also https://math.ryerson.ca/~niushan/Stieltjes-integrals.pdf [4] and Measure and Integration [5], Wheeden and Zygmund, for some facts about Riemann-Stieltjes and Lebesgue integrals.
 Here I am stating the results in terms of interval integrals, since it is what I need and the RS integral is equal to the Lebesgue one if one of the functions is increasing and right continuous and the other is bounded and measurable (see 4.1 in the previous link).
 To prove the general result it may be better to develop a theory of the Riemann-Stieltjes integral in mathlib and then prove the results for that integral and translate them for the lebesgue integral when possible.
+
+To be sure that the result is correct:
+Our integral is the same as the Lebesgue-Stieltjes integral defined in chapter 11.3 of [5], theorem 11.11 in [4] assures us that this integral corresponds to the Riemann-Stieltjes one in the case of a monotone right-continuous function and a bounded Borel-measurable one, if the Riemann-Stieltjes integral exists.
+Then theorem 4.7 in [2] says that for `f α : ℝ → ℝ` such that `f` is Rieman-Stieltjes integrable with respect to `α` on `[a, b]` then `α` is Riemann-Stieltjes integrable with respect to `f` on `[a, b]` and `∫ x in a..b, f x ∂α + ∫ x in a..b, α x ∂f = f b * α b - f a * α a `.
+Moreover theorem 7.27 of [2] says that if `f` is continuous on `[a, b]` and `α` is of bounded variation on `[a, b]` then `f` is Riemann-Stieltjes integrable with respect to `α` on `[a, b]`, the same is true if `f` is of bounded variation and `α` is continuous.
+
+In our case both functions are Stieltjes functions, hence they are of bounded variation, bounded on finite intervals and Borel measurable. However we also need to ask for one of the functions to be continuous, otherwise the Riemann-Stieltjes integral may not be true, for example if `f` and `α` have a common point of left discontinuity (see theorem 7.29 in [2]).
 -/
 -- #check intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right --one of the versions of the integration by parts that is currently in mathlib.
 
-lemma integral_stieltjes_meas_by_parts (f g : StieltjesFunction) (a b : ℝ) :
+lemma integral_stieltjes_meas_by_parts (f g : StieltjesFunction) (a b : ℝ)
+    (hf : ContinuousOn f (Set.Icc a b)) :
     ∫ x in a..b, f x ∂g.measure = (f b) * (g b) - (f a) * (g a) - ∫ x in a..b, g x ∂f.measure := by
   sorry

TestingLowerBounds/ForMathlib/CountableOrCountablyGenerated.lean

@@ -4,17 +4,24 @@ namespace MeasurableSpace
 
 variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
 
-
+-- PRed, see #15418
 lemma countable_left_of_prod_of_nonempty [Nonempty β] (h : Countable (α × β)) : Countable α := by
   contrapose h
   rw [not_countable_iff] at *
   infer_instance
 
+-- PRed, see #15418
 lemma countable_right_of_prod_of_nonempty [Nonempty α] (h : Countable (α × β)) : Countable β := by
   contrapose h
   rw [not_countable_iff] at *
   infer_instance
 
+-- PRed, see #15418
+instance [hα : CountableOrCountablyGenerated α γ] [hβ : CountableOrCountablyGenerated β γ] :
+    CountableOrCountablyGenerated (α × β) γ := by
+  rcases hα with (hα | hα) <;> rcases hβ with (hβ | hβ) <;> infer_instance
+
+-- PRed, see #15418
 lemma countableOrCountablyGenerated_left_of_prod_left_of_nonempty [Nonempty β]
     [h : CountableOrCountablyGenerated (α × β) γ] :
     CountableOrCountablyGenerated α γ := by
@@ -23,6 +30,7 @@ lemma countableOrCountablyGenerated_left_of_prod_left_of_nonempty [Nonempty β]
     infer_instance
   · infer_instance
 
+-- PRed, see #15418
 lemma countableOrCountablyGenerated_right_of_prod_left_of_nonempty [Nonempty α]
     [h : CountableOrCountablyGenerated (α × β) γ] :
     CountableOrCountablyGenerated β γ := by
@@ -61,9 +69,10 @@ lemma countableOrCountablyGenerated_left_of_prod_right_of_nonempty [Nonempty γ]
   · have := countablyGenerated_left_of_prod_of_nonempty h
     infer_instance
 
-instance [Countable (α × β)] : Countable (β × α) :=
-  Countable.of_equiv _ (Equiv.prodComm α β)
+-- PRed, see #15418
+instance [Countable (α × β)] : Countable (β × α) := Countable.of_equiv _ (Equiv.prodComm α β)
 
+-- PRed, see #15418
 instance [h : CountableOrCountablyGenerated (α × β) γ] :
     CountableOrCountablyGenerated (β × α) γ := by
   rcases h with (h | h)
@@ -74,10 +83,4 @@ instance [h : CountableOrCountablyGenerated (α × β) γ] :
 instance [CountablyGenerated (α × β)] : CountablyGenerated (β × α) := by
   sorry
 
-instance [h : CountableOrCountablyGenerated (α × β) γ] :
-    CountableOrCountablyGenerated (β × α) γ := by
-  rcases h with (h | h)
-  · exact ⟨Or.inl inferInstance⟩
-  · exact ⟨Or.inr h⟩
-
 end MeasurableSpace

TestingLowerBounds/ForMathlib/Indicator.lean

@@ -7,7 +7,7 @@ variable {α M : Type*} [Preorder M] [One M] {s : Set α} {f g : α → M} {a :
 
 namespace Set
 
---PR this to mathlib, just before `Set.mulIndicator_le_mulIndicator`.
+--PRed, see #15437
 @[to_additive]
 lemma mulIndicator_le_mulIndicator' (h : a ∈ s → f a ≤ g a) :
     mulIndicator s f a ≤ mulIndicator s g a :=

TestingLowerBounds/ForMathlib/Integrable_of_empty.lean

@@ -2,26 +2,29 @@ import Mathlib.MeasureTheory.Integral.Bochner
 
 open Filter
 
---TODO: put this in mathlib, maybe just after:
--- #check Integrable.of_finite
-
 namespace MeasureTheory
 
+--PRed, see #15459
 lemma Integrable.of_isEmpty {α β : Type*} [MeasurableSpace α] [NormedAddCommGroup β]
     [IsEmpty α] (f : α → β) (μ : Measure α) : Integrable f μ := Integrable.of_finite μ f
 
+--PRed, see #15459
 @[simp]
 lemma Integrable.of_isEmpty_codomain {α β : Type*} [MeasurableSpace α] [NormedAddCommGroup β]
     [IsEmpty β] (f : α → β) (μ : Measure α) : Integrable f μ :=
   have : IsEmpty α := f.isEmpty
   Integrable.of_isEmpty f μ
 
---TODO: put this in mathlib, maybe just after:
--- #check integral_eq_zero_of_ae
-
+--PRed, see #15459
 @[simp]
 lemma integral_of_isEmpty {α β : Type*} [MeasurableSpace α] [NormedAddCommGroup β]
     [NormedSpace ℝ β] [IsEmpty α] (f : α → β) (μ : Measure α) : ∫ x, f x ∂μ = 0 :=
   integral_eq_zero_of_ae <| eventually_of_forall (IsEmpty.forall_iff.mpr True.intro)
 
+--PRed, see #15459
+@[simp]
+lemma integral_of_isEmpty_codomain {α β : Type*} [MeasurableSpace α] [NormedAddCommGroup β]
+    [NormedSpace ℝ β] [IsEmpty β] (f : α → β) (μ : Measure α) : ∫ x, f x ∂μ = 0 :=
+  Subsingleton.eq_zero _
+
 end MeasureTheory

TestingLowerBounds/ForMathlib/IntegralCongr2.lean

@@ -15,20 +15,20 @@ namespace MeasureTheory
 variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α}
   {ν : Measure β} {κ : Kernel α β} {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
 
+--PRed, see #15460.
 lemma integral_congr_ae₂ {f g : α → β → G} (h : ∀ᵐ a ∂μ, f a =ᵐ[κ a] g a) :
     ∫ a, ∫ b, f a b ∂(κ a) ∂μ = ∫ a, ∫ b, g a b ∂(κ a) ∂μ := by
   apply integral_congr_ae
   filter_upwards [h] with a ha
   apply integral_congr_ae
   filter_upwards [ha] with b hb using hb
 
---change the name of this one
+--PRed as `ProbabilityTheory.Kernel.integral_congr_ae₂`, see #15460.
 lemma integral_congr_ae₂' {f g : α → β → G} (h : ∀ᵐ a ∂μ, f a =ᵐ[ν] g a) :
     ∫ a, ∫ b, f a b ∂ν ∂μ = ∫ a, ∫ b, g a b ∂ν ∂μ := by
   apply integral_congr_ae
   filter_upwards [h] with a ha
   apply integral_congr_ae
   filter_upwards [ha] with b hb using hb
 
--- #find_home! ProbabilityTheory.integral_congr_ae₂
 end MeasureTheory

TestingLowerBounds/ForMathlib/KernelConstComp.lean

@@ -10,12 +10,14 @@ variable {γ : Type*} {mγ : MeasurableSpace γ}
 --TODO: PR this to mathlib, after `comp_deterministic_eq_comap`
 -- #check comp_deterministic_eq_comap
 
+--PRed, see #15461
 lemma const_comp (μ : Measure γ) (κ : Kernel α β) :
     const β μ ∘ₖ κ = fun a ↦ (κ a) Set.univ • μ := by
   ext _ _ hs
   simp_rw [comp_apply' _ _ _ hs, const_apply, MeasureTheory.lintegral_const, Measure.smul_apply,
     smul_eq_mul, mul_comm]
 
+--PRed, see #15461
 @[simp]
 lemma const_comp' (μ : Measure γ) (κ : Kernel α β) [IsMarkovKernel κ] :
     const β μ ∘ₖ κ = const α μ := by

TestingLowerBounds/ForMathlib/KernelFstSnd.lean

@@ -17,6 +17,7 @@ variable {δ : Type*} {mδ : MeasurableSpace δ}
 
 --TODO: PR this to mathlib, a suitable place may be just under
 -- `ProbabilityTheory.Kernel.snd_swapRight`
+-- PRed, see #15466.
 
 --I try to reproduce the code that is already there for Kernel.fst and Kernel.snd, but in this case
 --the fst and snd are referred to the domain of the kernel, not the codomain

TestingLowerBounds/ForMathlib/Measure.lean

@@ -4,11 +4,11 @@ namespace MeasureTheory
 
 variable {α β : Type*} {m mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : Measure α}
 
-lemma measure_univ_le_add_compl (s : Set α) : μ Set.univ ≤ μ s + μ sᶜ := by
-  rw [← Set.union_compl_self s]
-  exact measure_union_le s sᶜ
+--PRed, see #15467
+lemma measure_univ_le_add_compl (s : Set α) : μ Set.univ ≤ μ s + μ sᶜ :=
+  s.union_compl_self ▸ measure_union_le s sᶜ
 
--- PR this, just after `Measure.sub_add_cancel_of_le`
+--PRed, see  #15468
 lemma Measure.add_sub_cancel [IsFiniteMeasure ν] : μ + ν - ν = μ := by
   ext1 s hs
   rw [sub_apply hs (Measure.le_add_left (le_refl _)), add_apply,

TestingLowerBounds/ForMathlib/MonotoneOnTendsto.lean

@@ -3,6 +3,7 @@ import Mathlib.Topology.Order.Basic
 open Set Filter Topology
 
 -- Put this in Mathlib, replacing `Monotone.tendsto_nhdsWithin_Iio`
+-- PRed, see #15470
 
 lemma MonotoneOn.tendsto_nhdsWithin_Ioo_left {α β : Type*} [LinearOrder α] [TopologicalSpace α]
     [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β]

TestingLowerBounds/ForMathlib/RnDeriv.lean

@@ -112,13 +112,13 @@ lemma rnDeriv_eq_zero_ae_of_zero_measure (ν : Measure α) {s : Set α} (hs : Me
   rw [← MeasureTheory.setLIntegral_eq_zero_iff hs (Measure.measurable_rnDeriv μ ν)]
   exact le_antisymm (hμ ▸ Measure.setLIntegral_rnDeriv_le s) (zero_le _)
 
---PR this, maybe it could go after `Measure.singularPart_restrict`?
+--PRed, see #15540
 lemma measure_sub_singularPart (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [IsFiniteMeasure μ] :
     μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν) := by
   nth_rw 1 [← rnDeriv_add_singularPart μ ν]
   exact add_sub_cancel
 
---PR this, maybe together with `Measure.measure_sub_singularPart`
+--PRed, see #15540
 lemma measure_sub_rnDeriv (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [IsFiniteMeasure μ] :
     μ - ν.withDensity (μ.rnDeriv ν) = μ.singularPart ν := by
   nth_rw 1 [← singularPart_add_rnDeriv μ ν]
@@ -298,19 +298,22 @@ lemma ae_integrable_of_ae_integrable_mul_rnDeriv {κ : α → Measure β} [Sigma
   exact isUnit_iff_ne_zero.mpr h_pos.ne'
 
 -- in mathlib this lemma could be put just before `MeasureTheory.Measure.rnDeriv_le_one_of_le`
+-- PRed, see #15473
 lemma rnDeriv_le_one_iff_le [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
     μ.rnDeriv ν ≤ᵐ[ν] 1 ↔ μ ≤ ν := by
   refine ⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩
   rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_apply', ← setLIntegral_one]
   exact setLIntegral_mono_ae aemeasurable_const (h.mono fun _ hh _ ↦ hh)
 
 -- in mathlib this lemma could be put just before `MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular`
+-- PRed, see #15473
 lemma rnDeriv_eq_one_iff_eq [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
     μ.rnDeriv ν =ᵐ[ν] 1 ↔ μ = ν := by
   refine ⟨fun h ↦ ?_, fun h ↦ h ▸ Measure.rnDeriv_self ν⟩
   rw [← withDensity_rnDeriv_eq _ _ hμν, MeasureTheory.withDensity_congr_ae h, withDensity_one]
 
 -- in mathlib this lemma could be put just after `Measure.rnDeriv_mul_rnDeriv`
+--PRed, see #15548.
 lemma _root_.MeasureTheory.Measure.rnDeriv_mul_rnDeriv' {κ : Measure α} [SigmaFinite μ]
     [SigmaFinite ν] [SigmaFinite κ] (hνκ : ν ≪ κ) :
     μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[ν] μ.rnDeriv κ := by
@@ -322,6 +325,7 @@ lemma _root_.MeasureTheory.Measure.rnDeriv_mul_rnDeriv' {κ : Measure α} [Sigma
   rw [hx1, Pi.add_apply, hx2, Pi.mul_apply, hx3, Pi.zero_apply, zero_add]
 
 --PR this to mathlib maybe just after `integral_toReal_rnDeriv` (we need to check that measure_sub_singularPart is imported there)?
+--PRed, see #15545.
 lemma _root_.MeasureTheory.Measure.integral_toReal_rnDeriv' {α : Type*} {m : MeasurableSpace α}
     {μ : Measure α} {ν : Measure α} [IsFiniteMeasure μ] [SigmaFinite ν] :
     ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν

TestingLowerBounds/ForMathlib/SetIntegral.lean

@@ -6,23 +6,27 @@ open scoped ENNReal
 variable {α E : Type*} [MeasurableSpace α] {μ ν : Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 -- PR this, just after `integral_rnDeriv_smul`
+--PRed, see #15551.
 lemma setIntegral_rnDeriv_smul [Measure.HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν)
     [SigmaFinite μ] {f : α → E} {s : Set α} (hs : MeasurableSet s) :
     ∫ x in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ x in s, f x ∂μ := by
   simp_rw [← integral_indicator hs, Set.indicator_smul, integral_rnDeriv_smul hμν]
 
 -- PR this, just after `integral_zero_measure`
+--PRed, see #15551.
 @[simp]
 theorem setIntegral_zero_measure
     (f : α → E) {μ : Measure α} {s : Set α} (hs : μ s = 0) :
     ∫ x in s, f x ∂μ = 0 := Measure.restrict_eq_zero.mpr hs ▸ integral_zero_measure f
 
 --PR these two lemmas to mathlib, just under `lintegral_eq_zero_iff`
+--PRed, see #15551.
 theorem setLIntegral_eq_zero_iff' {s : Set α} (hs : MeasurableSet s)
     {f : α → ℝ≥0∞} (hf : AEMeasurable f (μ.restrict s)) :
     ∫⁻ a in s, f a ∂μ = 0 ↔ ∀ᵐ x ∂μ, x ∈ s → f x = 0 :=
   (lintegral_eq_zero_iff' hf).trans (ae_restrict_iff' hs)
 
+--PRed, see #15551.
 theorem setLIntegral_eq_zero_iff {s : Set α} (hs : MeasurableSet s) {f : α → ℝ≥0∞}
     (hf : Measurable f) : ∫⁻ a in s, f a ∂μ = 0 ↔ ∀ᵐ x ∂μ, x ∈ s → f x = 0 :=
   setLIntegral_eq_zero_iff' hs hf.aemeasurable