Library UniMath.OrderTheory.DCPOs.Core.FubiniTheorem

1. Preliminary definitions
Definition monotone_function_app_l
           {X Y Z : dcpo}
           (f : monotone_function (X × Y) Z)
           (x : X)
  : monotone_function Y Z.
Show proof.
  simple refine (_ ,, _).
  - exact (λ y, f (x ,, y)).
  - abstract
      (intros y₁ y₂ p ; cbn ;
       apply f ;
       exact (refl_PartialOrder X x ,, p)).

Definition monotone_function_app_r
           {X Y Z : dcpo}
           (f : monotone_function (X × Y) Z)
           (y : Y)
  : monotone_function X Z.
Show proof.
  simple refine (_ ,, _).
  - exact (λ x, f (x ,, y)).
  - abstract
      (intros y₁ y₂ p ; cbn ;
       apply f ;
       exact (p ,, refl_PartialOrder Y y)).

Notation "f ·l x" := (monotone_function_app_l f x) (at level 60).
Notation "f ·r y" := (monotone_function_app_r f y) (at level 60).

Definition fubini_monotone_function_l
           {X Y Z : dcpo}
           (f : monotone_function (X × Y) Z)
           (D : directed_set (X × Y))
  : monotone_function X Z.
Show proof.
  refine ((λ x, _{π {{ D }}} (f ·l x)) ,, _).
  abstract
    (intros x₁ x₂ p ;
     use dcpo_lub_is_least ;
     cbn ;
     intro i ;
     use less_than_dcpo_lub ; [ exact i | ] ;
     cbn ;
     apply f ;
     split ; [ exact p | ] ;
     apply refl_PartialOrder).

Definition fubini_monotone_function_r
           {X Y Z : dcpo}
           (f : monotone_function (X × Y) Z)
           (D : directed_set (X × Y))
  : monotone_function Y Z.
Show proof.
  refine ((λ x, _{π {{ D }}} (f ·r x)) ,, _).
  abstract
    (intros x₁ x₂ p ;
     use dcpo_lub_is_least ;
     cbn ;
     intro i ;
     use less_than_dcpo_lub ; [ exact i | ] ;
     cbn ;
     apply f ;
     split ; [ | exact p ] ;
     apply refl_PartialOrder).

2. Fubini's theorem
Proposition monotone_prod_map_fubini_pair_l
            {X Y Z : dcpo}
            (f : monotone_function (X × Y) Z)
            (D : directed_set (X × Y))
  : _{D} f = _{π {{D}}} fubini_monotone_function_l f D.
Show proof.
  use (eq_lub Z (f {{ D }})).
  - apply is_least_upperbound_dcpo_comp_lub.
  - use make_dcpo_is_least_upperbound.
    + cbn ; intro i.
      use less_than_dcpo_lub.
      * exact i.
      * cbn.
        use less_than_dcpo_lub.
        ** exact i.
        ** apply refl_PartialOrder.
    + intros x' Hx'.
      use dcpo_lub_is_least ; cbn ; cbn in Hx'.
      intro i.
      use dcpo_lub_is_least ; cbn.
      intro j.
      assert (H := is_directed_top (directed_set_is_directed D) i j).
      revert H.
      use factor_through_squash.
      {
        apply propproperty.
      }
      intros kH.
      induction kH as [ k [ H₁ H₂ ]].
      refine (trans_PartialOrder Z _ (Hx' k)).
      apply f.
      split.
      * exact (pr1 H₁).
      * exact (pr2 H₂).

Proposition monotone_prod_map_fubini_pair_r
            {X Y Z : dcpo}
            (f : monotone_function (X × Y) Z)
            (D : directed_set (X × Y))
  : _{D} f = _{π {{D}}} fubini_monotone_function_r f D.
Show proof.
  use (eq_lub Z (f {{ D }})).
  - apply is_least_upperbound_dcpo_comp_lub.
  - use make_dcpo_is_least_upperbound.
    + cbn ; intro i.
      use less_than_dcpo_lub.
      * exact i.
      * cbn.
        use less_than_dcpo_lub.
        ** exact i.
        ** apply refl_PartialOrder.
    + intros x' Hx'.
      use dcpo_lub_is_least ; cbn ; cbn in Hx'.
      intro i.
      use dcpo_lub_is_least ; cbn.
      intro j.
      assert (H := is_directed_top (directed_set_is_directed D) i j).
      revert H.
      use factor_through_squash.
      {
        apply propproperty.
      }
      intros kH.
      induction kH as [ k [ H₁ H₂ ]].
      refine (trans_PartialOrder Z _ (Hx' k)).
      apply f.
      use prod_dcpo_le ; cbn.
      * exact (pr1 H₂).
      * exact (pr2 H₁).

Proposition monotone_fubini_swap
            {X Y Z : dcpo}
            (f : monotone_function (X × Y) Z)
            (D : directed_set (X × Y))
  : _{π {{D}}} fubini_monotone_function_l f D
    =
    _{π {{D}}} fubini_monotone_function_r f D.
Show proof.
  rewrite <- monotone_prod_map_fubini_pair_l.
  rewrite <- monotone_prod_map_fubini_pair_r.
  apply idpath.

Proposition monotone_fubini_swap'
            {X Y Z : dcpo}
            (D₁ : directed_set X)
            (D₂ : directed_set Y)
            (f : monotone_function (X × Y) Z)
  : _{D₁} (fubini_monotone_function_l f (prod_directed_set D₁ D₂))
    =
    _{D₂} (fubini_monotone_function_r f (prod_directed_set D₁ D₂)).
Show proof.
  refine (_ @ monotone_fubini_swap f (prod_directed_set D₁ D₂) @ _).
  - use antisymm_dcpo.
    + use dcpo_lub_is_least.
      cbn ; intro i.
      use dcpo_lub_is_least.
      cbn ; intro j.
      use less_than_dcpo_lub.
      * exact (i ,, pr2 j).
      * cbn.
        use less_than_dcpo_lub.
        ** exact (i ,, pr2 j).
        ** cbn.
           apply refl_dcpo.
    + use dcpo_lub_is_least.
      cbn ; intro i.
      use dcpo_lub_is_least.
      cbn ; intro j.
      use less_than_dcpo_lub.
      * exact (pr1 i).
      * cbn.
        use less_than_dcpo_lub.
        ** exact j.
        ** cbn.
           apply refl_dcpo.
  - use antisymm_dcpo.
    + use dcpo_lub_is_least.
      cbn ; intro i.
      use dcpo_lub_is_least.
      cbn ; intro j.
      use less_than_dcpo_lub.
      * exact (pr2 i).
      * cbn.
        use less_than_dcpo_lub.
        ** exact j.
        ** cbn.
           apply refl_dcpo.
    + use dcpo_lub_is_least.
      cbn ; intro i.
      use dcpo_lub_is_least.
      cbn ; intro j.
      use less_than_dcpo_lub.
      * exact (pr1 j ,, i).
      * cbn.
        use less_than_dcpo_lub.
        ** exact (pr1 j ,, i).
        ** cbn.
           apply refl_dcpo.