Mathlib.Probability.Kernel

theorem compProd_map_snd_apply {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (κ₁ : Kernel α β) (κ₂ : Kernel (α × β) γ) [IsSFiniteKernel κ₁] [IsSFiniteKernel κ₂] (a : α) : ((κ₁ ⊗ₖ κ₂).map snd) a = (κ₂.sectR a) ∘ₘ (κ₁ a) := by rw [Kernel.map_apply _ measurable_snd, Kernel.compProd_apply_eq_compProd_sectR, ← Measure.snd, Measure.snd_compProd]

theorem mechanismKernel_apply (νₗ : Measure γ) [SFinite νₗ] {Φ : β × γ → δ} (hΦ : Measurable Φ) (o : β) : mechanismKernel νₗ Φ o = νₗ.map (fun l => Φ (o, l)) := by unfold mechanismKernel rw [ProbabilityTheory.Kernel.map_apply _ hΦ, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.id_apply, ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.dirac_prod, MeasureTheory.Measure.map_map hΦ measurable_prodMk_left] rfl

theorem instIsMarkovKernelMechanismKernel (νₗ : Measure γ) [IsProbabilityMeasure νₗ] {Φ : β × γ → δ} (hΦ : Measurable Φ) : IsMarkovKernel (mechanismKernel νₗ Φ) := by unfold mechanismKernel exact ProbabilityTheory.Kernel.IsMarkovKernel.map _ hΦ

theorem measurable_kernelUnitQuantile (κ : Kernel S ℝ) [IsMarkovKernel κ] : Measurable (uncurry (kernelUnitQuantile κ)) := by refine measurable_of_Ioi fun a ↦ ?_ simp only [preimage, uncurry, mem_Ioi] have h_monotone s : Monotone (fun x : unitInterval ↦ (κ s).real (Icc (0 : ℝ) x)) := fun x y hxy ↦ measureReal_mono (by gcongr) have sSup_eq_iUnion_rat : {x : S × unitInterval | a < kernelUnitQuantile κ x.1 x.2} = ⋃ (q : ℚ) (hqI : (↑q : ℝ) ∈ unitInterval) (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc (0 : ℝ) ((⟨(q : ℝ), hqI⟩ : unitInterval) : ℝ)) < e.2} := by ext e simp_all only [lt_sSup_iff, mem_ofPred_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg, mem_iUnion, exists_prop, exists_and_left, kernelUnitQuantile] constructor · rintro ⟨y, y_mem, hyI, (hy : a.1 < y)⟩ obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy have hq0 : 0 ≤ q := by exact (Rat.cast_nonneg (K := ℝ)).mp (a.2.1.trans hqa.le) have hqI : (q : ℝ) ∈ unitInterval := ⟨a.2.1.trans hqa.le, hqy.le.trans hyI.2⟩ refine ⟨q, ⟨hq0, hqI.2⟩, hqa, lt_of_lt_of_le' y_mem ?_⟩ exact h_monotone e.1 (a := ⟨(q : ℝ), hqI⟩) (b := ⟨y, hyI⟩) hqy.le · intro he obtain ⟨q, hqI, hqa, h⟩ := he exact ⟨q, h, ⟨by simp [hqI.1], hqI.2⟩, hqa⟩ rw [sSup_eq_iUnion_rat] refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_))) refine measurableSet_lt ?_ measurable_snd.subtype_val simp_rw [measureReal_def] have hκ := κ.measurable_coe (s := Icc (0 : ℝ) ((⟨(b : ℝ), bI⟩ : unitInterval) : ℝ)) measurableSet_Icc fun_prop

theorem measurable_quantileRealization (κ : Kernel S ℝ) [IsMarkovKernel κ] : Measurable (quantileRealization κ) := by change Measurable (fun p : S × ℝ ↦ ((kernelUnitQuantile κ p.1 (projIcc (0 : ℝ) 1 zero_le_one p.2) : unitInterval) : ℝ)) exact measurable_subtype_coe.comp <| (measurable_kernelUnitQuantile κ).comp <| measurable_fst.prodMk ((continuous_projIcc (a := (0 : ℝ)) (b := 1) (h := zero_le_one)).measurable.comp measurable_snd)

@[fun_prop] theorem measurable_quantileRealization_section (κ : Kernel S ℝ) [IsMarkovKernel κ] (s : S) : Measurable (fun u : ℝ => quantileRealization κ (s, u)) := by exact (measurable_quantileRealization κ).comp (measurable_const.prodMk measurable_id)

theorem map_kernelUnitQuantile (κ : Kernel S ℝ) [IsMarkovKernel κ] (hκ : SupportedOnUnitInterval κ) (s : S) : Measure.map (fun u : unitInterval => (kernelUnitQuantile κ s u : ℝ)) volume = κ s := by let f := fun u : unitInterval => (kernelUnitQuantile κ s u : ℝ) have hf : Measurable f := measurable_subtype_coe.comp (measurable_kernelUnitQuantile κ).of_uncurry_left have hκ_compl : κ s (Icc (0 : ℝ) 1)ᶜ = 0 := by rw [measure_compl measurableSet_Icc (measure_ne_top (κ s) _), hκ s, measure_univ] simp have hκ_ae : ∀ᵐ y ∂κ s, y ∈ Icc (0 : ℝ) 1 := by rw [ae_iff] exact hκ_compl have hκ_Iic (z : unitInterval) : κ s (Iic (z : ℝ)) = κ s (Icc 0 (z : ℝ)) := by apply measure_congr refine hκ_ae.mono ?_ intro y hy apply propext exact ⟨fun h ↦ ⟨hy.1, h⟩, And.right⟩ refine (Measure.map f volume).ext_of_Iic (κ s) fun x ↦ ?_ rw [Measure.map_apply hf measurableSet_Iic] change volume {u : unitInterval | (kernelUnitQuantile κ s u : ℝ) ≤ x} = κ s (Iic x) by_cases hx0 : x < 0 · have hpre : {u : unitInterval | (kernelUnitQuantile κ s u : ℝ) ≤ x} = ∅ := by ext u simp only [mem_ofPred_eq, mem_empty_iff_false, iff_false] exact not_le.mpr (hx0.trans_le (kernelUnitQuantile κ s u).property.1) have hnull : κ s (Iic x) = 0 := by refine measure_mono_null ?_ hκ_compl intro y hy simp only [mem_Iic] at hy simp only [mem_compl_iff, mem_Icc, not_and_or] exact inl (not_le.mpr (hy.trans_lt hx0)) rw [hpre, measure_empty, hnull] · have hx0' : 0 ≤ x := le_of_not_gt hx0 by_cases hx1 : x ≤ 1 · let xI : unitInterval := ⟨x, hx0', hx1⟩ have hIic : κ s (Iic x) = κ s (Icc 0 x) := hκ_Iic xI have κ_in_I : ((κ s).real (Icc (0 : ℝ) x)) ∈ unitInterval := ⟨measureReal_nonneg, measureReal_le_one⟩ rw [hIic, ← ofReal_measureReal (measure_ne_top (κ s) _), ← unitInterval.volume_Iic ⟨_, κ_in_I⟩] congr with ξ constructor · intro (hξ : kernelUnitQuantile κ s ξ ≤ xI) change ξ ≤ (κ s).real (Icc (0 : ℝ) x) by_cases hx : xI = 1 · have hx' : x = 1 := congrArg val hx rw [hx', measureReal_def, hκ s] simpa using ξ.2.2 let g := fun y : unitInterval ↦ (κ s).real (Icc (0 : ℝ) y) let nebot : NeBot (𝓝[>] xI) := by refine nhdsGT_neBot_of_exists_gt ?_ use 1 exact lt_of_le_of_ne xI.2.2 hx refine le_of_tendsto_of_tendsto (b := 𝓝[>] xI) (g := g) continuousWithinAt_const ?_ ?_ · let h := cdf (κ s) have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous (xI : ℝ)) have hreal (y : unitInterval) : (κ s).real (Icc (0 : ℝ) (y : ℝ)) = h (y : ℝ) := by change (κ s).real (Icc (0 : ℝ) (y : ℝ)) = cdf (κ s) (y : ℝ) rw [ProbabilityTheory.cdf_eq_real, measureReal_def, measureReal_def, hκ_Iic y] simp_rw [g, hreal] rw [hreal xI] exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy) · refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_ by_contra! h simp only [sSup_le_iff, kernelUnitQuantile] at hξ specialize hξ y h grind · intro (hξ : ξ ≤ (κ s).real (Icc (0 : ℝ) x)) change kernelUnitQuantile κ s ξ ≤ xI simp only [sSup_le_iff, kernelUnitQuantile] intro c hc by_contra! h have h_lt : ¬(κ s).real (Icc (0 : ℝ) x) ≤ (κ s).real (Icc (0 : ℝ) c) := not_le.mpr (lt_of_le_of_lt' hξ hc) refine h_lt ?_ refine measureReal_mono ?_ intro z hz exact ⟨hz.1, hz.2.trans (by exact_mod_cast h.le)⟩ · have hx1' : 1 < x := lt_of_not_ge hx1 have hpre : {u : unitInterval | (kernelUnitQuantile κ s u : ℝ) ≤ x} = univ := by ext u simp only [mem_ofPred_eq, mem_univ, iff_true] exact (kernelUnitQuantile κ s u).property.2.trans hx1'.le have hfull : κ s (Iic x) = 1 := by calc κ s (Iic x) = κ s univ := by apply measure_congr refine hκ_ae.mono ?_ intro y hy exact propext ⟨fun _ ↦ mem_univ y, fun _ ↦ hy.2.trans hx1'.le⟩ _ = 1 := measure_univ rw [hpre, measure_univ, hfull]