OAI/Analysis/CoulombTransport/BranchCoupling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem356.branchGraph line 12

   Source documentation

   A graph with all three coordinates explicitly specified.

   def branchGraph (f g h : E3 → E3) : E3 → Triple := fun x => (f x, (g x, h x))

   Mentions: OAI.Problem356.E3, OAI.Problem356.Triple

2. lemma OAI.Problem356.measurable_branchGraph line 14
3. def OAI.Problem356.branchMarginal line 19

   Source documentation

   The marginal used by the two-branch construction.

   def branchMarginal (nu : Measure E3) (H1 H2 H3 H4 : E3 → E3) : Measure E3 :=
   …

   Mentions: OAI.Problem356.E3

4. def OAI.Problem356.branchCoupling line 25

   Source documentation

   Each branch is averaged over its three cyclic coordinate orderings.

   def branchCoupling (nu : Measure E3) (H1 H2 H3 H4 : E3 → E3) : Measure Triple :=
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.Triple

5. lemma OAI.Problem356.map_tripleFst_branchGraph line 34
6. lemma OAI.Problem356.map_tripleSnd_branchGraph line 40
7. lemma OAI.Problem356.map_tripleThd_branchGraph line 47
8. lemma OAI.Problem356.six_smul_group line 54
9. lemma OAI.Problem356.map_tripleFst_branchCoupling line 68
10. lemma OAI.Problem356.map_tripleSnd_branchCoupling line 83
11. lemma OAI.Problem356.map_tripleThd_branchCoupling line 101
12. lemma OAI.Problem356.isProbabilityMeasure_branchCoupling line 119
13. theorem OAI.Problem356.isThreeCoupling_branchCoupling line 136

    Source documentation

    The explicit two-branch mixture is an admissible coupling of its five-component marginal.

    theorem isThreeCoupling_branchCoupling (nu : Measure E3) [IsProbabilityMeasure nu]
        {H1 H2 H3 H4 : E3 → E3}
        (h1 : Measurable H1) (h2 : Measurable H2) (h3 : Measurable H3)
        (h4 : Measurable H4) :
        IsThreeCoupling (branchMarginal nu H1 H2 H3 H4) (branchCoupling nu H1 H2 H3 H4) :=
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.IsThreeCoupling, OAI.Problem356.branchMarginal, OAI.Problem356.branchCoupling

14. lemma OAI.Problem356.isProbabilityMeasure_branchMarginal line 146
15. theorem OAI.Problem356.ae_branchCoupling line 156

    Source documentation

    Any measurable cyclically invariant property holding on the two branches also holds almost everywhere for their explicit coupling.

    theorem ae_branchCoupling (nu : Measure E3) {H1 H2 H3 H4 : E3 → E3}
        (h1 : Measurable H1) (h2 : Measurable H2) (h3 : Measurable H3)
        (h4 : Measurable H4) {P : Triple → Prop} (hP : MeasurableSet {t | P t})
        (hcycle : ∀ x y z, P (x, (y, z)) → P (y, (z, x)))
        (h12 : ∀ᵐ x ∂nu, P (x, (H1 x, H2 x)))
        (h34 : ∀ᵐ x ∂nu, P (x, (H3 x, H4 x))) :
        ∀ᵐ t ∂branchCoupling nu H1 H2 H3 H4, P t := by
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.branchCoupling