feat(probability/kernel/cond_cdf): conditional cumulative distributio…

…n function (#18988)

We define `cond_cdf ρ : α → stieltjes_function`, the conditional cdf of `ρ : measure (α × ℝ)`, and prove its main properties: it is monotone and right-continuous with limit 0 at -∞ and limit 1 at +∞; for all `x : ℝ`, `a ↦ cond_cdf ρ a x` is measurable; for all `x : ℝ` and measurable set `s`, it satisfies `∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x)`

src/measure_theory/constructions/borel_space/basic.lean

@@ -148,6 +148,23 @@ end
 lemma borel_eq_generate_from_Ioi : borel α = generate_from (range Ioi) :=
 @borel_eq_generate_from_Iio αᵒᵈ _ (by apply_instance : second_countable_topology α) _ _
 
+lemma borel_eq_generate_from_Iic : borel α = measurable_space.generate_from (range Iic) :=
+begin
+  rw borel_eq_generate_from_Ioi,
+  refine le_antisymm _ _,
+  { refine measurable_space.generate_from_le (λ t ht, _),
+    obtain ⟨u, rfl⟩ := ht,
+    rw ← compl_Iic,
+    exact (measurable_space.measurable_set_generate_from (mem_range.mpr ⟨u, rfl⟩)).compl, },
+  { refine measurable_space.generate_from_le (λ t ht, _),
+    obtain ⟨u, rfl⟩ := ht,
+    rw ← compl_Ioi,
+    exact (measurable_space.measurable_set_generate_from (mem_range.mpr ⟨u, rfl⟩)).compl, },
+end
+
+lemma borel_eq_generate_from_Ici : borel α = measurable_space.generate_from (range Ici) :=
+@borel_eq_generate_from_Iic αᵒᵈ _ _ _ _
+
 end order_topology
 
 lemma borel_comap {f : α → β} {t : topological_space β} :

src/measure_theory/measure/stieltjes.lean

@@ -29,6 +29,47 @@ section move_this
 open filter set
 open_locale topology
 
+lemma infi_Ioi_eq_infi_rat_gt {f : ℝ → ℝ} (x : ℝ) (hf : bdd_below (f '' Ioi x))
+  (hf_mono : monotone f) :
+  (⨅ r : Ioi x, f r) = ⨅ q : {q' : ℚ // x < q'}, f q :=
+begin
+  refine le_antisymm _ _,
+  { haveI : nonempty {r' : ℚ // x < ↑r'},
+    { obtain ⟨r, hrx⟩ := exists_rat_gt x,
+      exact ⟨⟨r, hrx⟩⟩, },
+    refine le_cinfi (λ r, _),
+    obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop,
+    refine cinfi_set_le hf (hxy.trans _),
+    exact_mod_cast hyr, },
+  { refine le_cinfi (λ q, _),
+    have hq := q.prop,
+    rw mem_Ioi at hq,
+    obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq,
+    refine (cinfi_le _ _).trans _,
+    { exact ⟨y, hxy⟩, },
+    { refine ⟨hf.some, λ z, _⟩,
+      rintros ⟨u, rfl⟩,
+      suffices hfu : f u ∈ f '' Ioi x, from hf.some_spec hfu,
+      exact ⟨u, u.prop, rfl⟩, },
+    { refine hf_mono (le_trans _ hyq.le),
+      norm_cast, }, },
+end
+
+-- todo after the port: move to topology/algebra/order/left_right_lim
+lemma right_lim_eq_of_tendsto {α β : Type*} [linear_order α] [topological_space β]
+  [hα : topological_space α] [h'α : order_topology α] [t2_space β]
+  {f : α → β} {a : α} {y : β} (h : 𝓝[>] a ≠ ⊥) (h' : tendsto f (𝓝[>] a) (𝓝 y)) :
+  function.right_lim f a = y :=
+@left_lim_eq_of_tendsto αᵒᵈ _ _ _ _ _ _ f a y h h'
+
+-- todo after the port: move to topology/algebra/order/left_right_lim
+lemma right_lim_eq_Inf {α β : Type*} [linear_order α] [topological_space β]
+  [conditionally_complete_linear_order β] [order_topology β] {f : α → β}
+  (hf : monotone f) {x : α}
+  [topological_space α] [order_topology α] (h : 𝓝[>] x ≠ ⊥) :
+  function.right_lim f x = Inf (f '' (Ioi x)) :=
+right_lim_eq_of_tendsto h (hf.tendsto_nhds_within_Ioi x)
+
 -- todo after the port: move to order/filter/at_top_bot
 lemma exists_seq_monotone_tendsto_at_top_at_top (α : Type*) [semilattice_sup α] [nonempty α]
   [(at_top : filter α).is_countably_generated] :
@@ -172,6 +213,33 @@ lemma mono : monotone f := f.mono'
 
 lemma right_continuous (x : ℝ) : continuous_within_at f (Ici x) x := f.right_continuous' x
 
+lemma right_lim_eq (f : stieltjes_function) (x : ℝ) :
+  function.right_lim f x = f x :=
+begin
+  rw [← f.mono.continuous_within_at_Ioi_iff_right_lim_eq, continuous_within_at_Ioi_iff_Ici],
+  exact f.right_continuous' x,
+end
+
+lemma infi_Ioi_eq (f : stieltjes_function) (x : ℝ) :
+  (⨅ r : Ioi x, f r) = f x :=
+begin
+  suffices : function.right_lim f x = ⨅ r : Ioi x, f r,
+  { rw [← this, f.right_lim_eq], },
+  rw [right_lim_eq_Inf f.mono, Inf_image'],
+  rw ← ne_bot_iff,
+  apply_instance,
+end
+
+lemma infi_rat_gt_eq (f : stieltjes_function) (x : ℝ) :
+  (⨅ r : {r' : ℚ // x < r'}, f r) = f x :=
+begin
+  rw ← infi_Ioi_eq f x,
+  refine (infi_Ioi_eq_infi_rat_gt _ _ f.mono).symm,
+  refine ⟨f x, λ y, _⟩,
+  rintros ⟨y, hy_mem, rfl⟩,
+  exact f.mono (le_of_lt hy_mem),
+end
+
 /-- The identity of `ℝ` as a Stieltjes function, used to construct Lebesgue measure. -/
 @[simps] protected def id : stieltjes_function :=
 { to_fun := id,