Rel Triple' iff coupling Post

theorem relTriple'_iff_couplingPost    {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} :    RelTriple' oa ob R ↔ CouplingPost oa ob R := by  constructor  · intro h    classical    letI : DecidableEq α := Classical.decEq α    letI : DecidableEq β := Classical.decEq β    unfold RelTriple' at h    by_cases hne : Nonempty (SPMF.Coupling (𝒟[oa]) (𝒟[ob]))    · let A := {a // a ∈ finSupport oa}      let B := {b // b ∈ finSupport ob}      letI : DecidableEq A := Classical.decEq A      letI : DecidableEq B := Classical.decEq B      letI : Fintype A := inferInstance      letI : Fintype B := inferInstance      have hA_nonempty : (finSupport oa).Nonempty := finSupport_nonempty_of_liftM_PMF oa      have hB_nonempty : (finSupport ob).Nonempty := finSupport_nonempty_of_liftM_PMF ob      let a₀ : A := ⟨hA_nonempty.choose, hA_nonempty.choose_spec⟩      let b₀ : B := ⟨hB_nonempty.choose, hB_nonempty.choose_spec⟩      let packA : α → A := fun a => if ha : a ∈ finSupport oa then ⟨a, ha⟩ else a₀      let packB : β → B := fun b => if hb : b ∈ finSupport ob then ⟨b, hb⟩ else b₀      let packPair : α × β → A × B := fun z => (packA z.1, packB z.2)      let valPair : A × B → α × β := fun z => (z.1.1, z.2.1)      let pa : SPMF A := packA <$> 𝒟[oa]      let pb : SPMF B := packB <$> 𝒟[ob]      have hvalA : Subtype.val <$> pa = 𝒟[oa] :=        evalDist_map_val_pack_eq Subtype.val packA fun a ha => by simp [packA, ha]      have hvalB : Subtype.val <$> pb = 𝒟[ob] :=        evalDist_map_val_pack_eq Subtype.val packB fun b hb => by simp [packB, hb]      have hsub_nonempty : Nonempty (SPMF.Coupling pa pb) := by        rcases hne with ⟨c₀⟩        exact ⟨⟨packPair <$> c₀.1, isCoupling_map_pair packA packB c₀⟩⟩      let fSub : Option (A × B) → ℝ≥0∞        | none => 0        | some z => RelPost.indicator R z.1.1 z.2.1      have hfSub : ∀ z, fSub z ≠ ⊤ := by        rintro (_ | z)        · simp [fSub]        · by_cases hR : R z.1.1 z.2.1 <;> simp [fSub, RelPost.indicator, hR]      obtain ⟨cMaxSub, hMaxSub⟩ := SPMF.exists_max_coupling        (p := pa) (q := pb) fSub hfSub hsub_nonempty (isCompact_couplings_set pa pb)      have hsub_obj :          ∀ c : SPMF.Coupling pa pb,            (∑' z : Option (A × B), c.1.1 z * fSub z) =              Pr[ fun z : A × B => R z.1.1 z.2.1 | (c.1 : SPMF (A × B))] := by        intro c        rw [probEvent_eq_tsum_ite, tsum_option _ ENNReal.summable]        simp only [RelPost.indicator, mul_zero, mul_ite, mul_one, tsum_fintype, zero_add, fSub]        rfl      have hlift_obj :          ∀ c : SPMF.Coupling (𝒟[oa]) (𝒟[ob]),            Pr[ fun z : A × B => R z.1.1 z.2.1 | packPair <$> c.1] =              Pr[ fun z : α × β => R z.1 z.2 | c.1] := by        intro c        rw [probEvent_map]        refine probEvent_ext fun z hz => ?_        have hzfst : z.1 ∈ support 𝒟[oa] := by rw [← c.2.map_fst, support_map]; exact ⟨z, hz, rfl⟩        have hzsnd : z.2 ∈ support 𝒟[ob] := by rw [← c.2.map_snd, support_map]; exact ⟨z, hz, rfl⟩        simp [packPair, packA, packB,          mem_finSupport_of_mem_support_evalDist (oa := oa) (x := z.1) hzfst,          mem_finSupport_of_mem_support_evalDist (oa := ob) (x := z.2) hzsnd]      have hpush :          SPMF.IsCoupling (valPair <$> cMaxSub.1) (𝒟[oa]) (𝒟[ob]) := by        constructor        · simpa [valPair] using            (congrArg (fun p : SPMF A => Subtype.val <$> p) cMaxSub.2.map_fst).trans hvalA        · simpa [valPair] using            (congrArg (fun p : SPMF B => Subtype.val <$> p) cMaxSub.2.map_snd).trans hvalB      let cMax : SPMF.Coupling (𝒟[oa]) (𝒟[ob]) := ⟨valPair <$> cMaxSub.1, hpush⟩      have hpush_obj :          Pr[ fun z : α × β => R z.1 z.2 | cMax.1] =            Pr[ fun z : A × B => R z.1.1 z.2.1 | cMaxSub.1] :=        probEvent_map (mx := cMaxSub.1) (f := valPair) (q := fun z : α × β => R z.1 z.2)      have hsub_le_max :          ∀ c : SPMF.Coupling pa pb,            Pr[ fun z : A × B => R z.1.1 z.2.1 | (c.1 : SPMF (A × B))] ≤              Pr[ fun z : A × B => R z.1.1 z.2.1 | (cMaxSub.1 : SPMF (A × B))] := by        intro c        rw [← hsub_obj c, ← hsub_obj cMaxSub]        exact (le_iSup (f := fun c' : SPMF.Coupling pa pb =>          ∑' z : Option (A × B), c'.1.1 z * fSub z) c).trans hMaxSub.le      have hupper :          eRelWP oa ob (RelPost.indicator R) ≤            Pr[ fun z : α × β => R z.1 z.2 | cMax.1] := by        unfold eRelWP        refine iSup_le fun c => ?_        let cLift : SPMF.Coupling pa pb := ⟨packPair <$> c.1, isCoupling_map_pair packA packB c⟩        calc          ∑' z, Pr[= z | c.1] * RelPost.indicator R z.1 z.2              = Pr[ fun z : α × β => R z.1 z.2 | c.1] := by                  simpa [RelPost.indicator] using                    indicator_objective_eq_probEvent (mx := c.1) (R := R)          _ = Pr[ fun z : A × B => R z.1.1 z.2.1 | packPair <$> c.1] :=                (hlift_obj c).symm          _ ≤ Pr[ fun z : α × β => R z.1 z.2 | cMax.1] := by            rw [hpush_obj]; exact hsub_le_max cLift      exact ⟨cMax, (probEvent_eq_one_iff (mx := cMax.1) (p := fun z : α × β => R z.1 z.2)).1        (le_antisymm probEvent_le_one (le_trans h hupper)) |>.2⟩    · haveI : IsEmpty (SPMF.Coupling (𝒟[oa]) (𝒟[ob])) := not_nonempty_iff.mp hne      simp [eRelWP] at h  · intro ⟨c, hc⟩    unfold RelTriple' eRelWP    refine le_iSup_of_le c <| le_of_eq ?_    rw [← coupling_tsum_probOutput_eq_one c]    refine tsum_congr fun z => ?_    by_cases hz : z ∈ support c.1    · simp [RelPost.indicator, hc z hz]    · simp [probOutput_eq_zero_of_not_mem_support hz]