Modification Multiplication for Probability Kernels

Stream: GibbsMeasure

[Fred Rajasekaran]

I'm currently working on the lemma IsModifier.mul in Specification.lean, and I've reached a point where the statement I'm trying to prove is true for Probability Kernels (i.e. all the induced measures have total mass one). I'm not entirely sure if the original statement of the lemma is true in general for all kernels the way we've defined them (still need to think about this), or if I've reached this point by not making use of all of the properties of specifications/modifiers.

Below is the Lean code I have so far (ignore the poor quality, I'll clean it up once I have a working proof). The bulk of the code is just rewriting all the densities as integrals, and then showing that the functions inside the integrals are equal.

The last goal before the sorry is "(((γ Λ₁) a).withDensity (ρ₁ Λ₁ * ρ₂ Λ₁)) b = b.indicator (fun x ↦ 1) a". Here, γ is a specification, so (γ Λ₁) is a proper kernel. This identity is equation (1.19) in Georgii's book (2nd edition) for proper probability kernels. For general kernels, we can use equation (1.18) with A being the entire space, and see that the right hand side should be multiplied by the measure of the entire space.

Right now, I think Specifications are defined as general kernels in the project and not as probability kernels specifically. Should I specify somehow that γ Λ₁ is a probability kernel in the statement? Or does anyone see where I'm missing something and can still prove it for general kernels?
@Kalle Kytölä @Yaël Dillies @Yan Yablonovskiy @Kin Yau James Wong

@[simp] lemma IsModifier.mul {ρ₁ ρ₂ : Finset S → (S → E) → ℝ≥0∞}
    (hρ₁ : γ.IsModifier ρ₁) (hρ₂ : (γ.modification ρ₁ hρ₁).IsModifier ρ₂) :
    γ.IsModifier (ρ₁ * ρ₂) where
  measurable Λ := (hρ₁.measurable _).mul (hρ₂.measurable _)
  isConsistent := by

    rw[IsConsistent]
    intros Λ₁ Λ₂ hsub

    have h_cons : (γ.modification ρ₁ hρ₁ Λ₁).comap id cylinderEvents_le_pi ∘ₖ (γ.modification ρ₁ hρ₁ Λ₂) = (γ.modification ρ₁ hρ₁ Λ₂) := by
      rw[(γ.modification ρ₁ hρ₁).isConsistent hsub]
    rw[modificationKer, modificationKer]

    simp [Kernel.comap, Kernel.comp]
    ext x s hs
    simp[Measure.bind]
    simp[Measure.join]
    rw[MeasureTheory.withDensity_mul]
    simp[Measure.ofMeasurable]
    have measure_eq_coe (α : Measure (S → E)) (s : Set (S → E)) (hs : MeasurableSet s) : α s = α.toOuterMeasure s :=
      rfl

    rw[measure_eq_coe]
    simp
    rw[inducedOuterMeasure]

    conv_rhs=>
      rw[Measure.withDensity]
    rw[Measure.ofMeasurable]
    rw[measure_eq_coe]
    simp
    rw[inducedOuterMeasure]
    --apply congr_arg₂
    congr
    apply congr_arg
    apply funext
    intro b
    apply funext
    intro hb
    rw[MeasureTheory.lintegral_map]
    rw[MeasureTheory.lintegral_withDensity_eq_lintegral_mul]
    rw[←MeasureTheory.lintegral_indicator]
    simp
    refine lintegral_congr ?_
    intro a
    have h_equal : (fun c ↦ (fun _ ↦ (1 : ENNReal)) c * (ρ₂ Λ₂) c) = ρ₂ Λ₂  :=by
      simp

    rw[←h_equal]
    rw[b.indicator_mul_left]
    simp
    rw[mul_comm]
    rw[ENNReal.mul_left_inj]

    sorry

[Yaël Dillies]

Sorry, I realise I never replied to your message, @Fred Rajasekaran! You should feel free to assume anything extra about the kernel. The book only talks about probability kernels

[Matteo Cipollina]

I've been working on some files in this PR and more recently have completed the sorry s in CondExp (It seems nobody was working on it but apologies if otherwise). If nobody is working on it, I'm going to make a try at LebesgueCondExp :)