LeanMachineLearning

ProbabilityTheory.Kernel.instDeterministicSFinKerHomOfIsMarkovKernel🔗

Instance

No docstring.

🔗theorem
ProbabilityTheory.Kernel.instDeterministicSFinKerHomOfIsMarkovKernel.{u_1,
    u_2, u_5}
  {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y]
  {SX SY : SFinKer} {ex : SFinKer.carrier SX ≃ᵐ X}
  {ey : SFinKer.carrier SY ≃ᵐ Y} {κ : Kernel X Y} [IsDeterministic κ]
  [IsMarkovKernel κ] : CategoryTheory.Deterministic (hom κ)
ProbabilityTheory.Kernel.instDeterministicSFinKerHomOfIsMarkovKernel.{u_1,
    u_2, u_5}
  {X : Type u_1} {Y : Type u_2}
  [MeasurableSpace X] [MeasurableSpace Y]
  {SX SY : SFinKer}
  {ex : SFinKer.carrier SX ≃ᵐ X}
  {ey : SFinKer.carrier SY ≃ᵐ Y}
  {κ : Kernel X Y} [IsDeterministic κ]
  [IsMarkovKernel κ] :
  CategoryTheory.Deterministic (hom κ)

Code

instance {κ : Kernel X Y} [IsDeterministic κ] [IsMarkovKernel κ] :
    Deterministic (hom (ex := ex) (ey := ey) κ)
Proof
by
  set κ_hom := hom (ex := ex) (ey := ey) κ
  have : IsDeterministic κ_hom.hom := by
    refine ⟨?_⟩
    ext a s hs
    simp only [hom, κ_hom]
    have := κ.parallelComp_self_comp_copy
    have := DFunLike.congr_fun (x := ex a) this
    have := DFunLike.congr_fun (x := ey.prodCongr ey '' s) this
    rw [comap_parallelComp_comap, map_parallelComp_map, comp_apply', comp_apply',
      copy, deterministic_apply, lintegral_dirac', comap_apply', map_apply', parallelComp_apply',
      lintegral_comap, lintegral_map]
    · rw [comp_apply', comp_apply', copy, deterministic_apply, lintegral_dirac',
        parallelComp_apply'] at this
      · convert this
        all_goals try rfl
        · ext y
          simp [MeasurableEquiv.prodCongr]
          aesop
        · simp only [copy, deterministic_apply]
          rw [Measure.dirac_apply', Measure.dirac_apply']
          · refine Set.indicator_eq_indicator ?_ rfl
            simp [MeasurableEquiv.prodCongr]
            aesop
          · exact (measurableSet_image (ey.prodCongr ey)).mpr hs
          · exact hs
      all_goals try measurability
      · exact Kernel.measurable_coe _ (by measurability)
    all_goals try measurability
    · exact Kernel.measurable_coe _ hs
    · exact Kernel.measurable_coe _ hs
  have : IsMarkovKernel κ_hom.hom :=
    have : IsMarkovKernel (κ.map ey.symm) :=
      IsMarkovKernel.map _ (by fun_prop)
    IsMarkovKernel.comap _ (by fun_prop)
  exact SX.deterministic_deterministic SY κ_hom.hom

Actions: Source · Open Issue

Meaning last changed in v4.34.0-rc2-1-g439785b (2026-08-23).

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 4 project declarations, 185 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.