Symmetrization.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.Cyclic.rotate line 13
Source documentation
The cyclic rotation of the three particles.
```
def rotate : Triple ≃ᵐ Triple where
…
```
Mentions: OAI.Problem356.Triple
def OAI.Problem356.Cyclic.symmetrize line 24
Source documentation
Averaging over the cyclic group already gives identical coordinate marginals.
```
def symmetrize (pi : Measure Triple) : Measure Triple :=
…
```
Mentions: OAI.Problem356.Triple
def OAI.Problem356.Cyclic.averageMarginal line 28
Source documentation
The common marginal of the cyclic average.
```
def averageMarginal (pi : Measure Triple) : Measure E3 :=
…
```
Mentions: OAI.Problem356.Triple, OAI.Problem356.E3
theorem OAI.Problem356.Cyclic.measurable_fst₃ line 32
theorem OAI.Problem356.Cyclic.measurable_snd₃ line 33
theorem OAI.Problem356.Cyclic.measurable_thd₃ line 34
theorem OAI.Problem356.Cyclic.map_fst_symmetrize line 36
theorem OAI.Problem356.Cyclic.map_snd_symmetrize line 44
theorem OAI.Problem356.Cyclic.map_thd_symmetrize line 54
theorem OAI.Problem356.Cyclic.symmetrize_probability line 64
theorem OAI.Problem356.Cyclic.symmetrize_isThreeCoupling line 73
theorem OAI.Problem356.Cyclic.ae_symmetrize_of_rotate_invariant line 80
Source documentation
A cyclically invariant property holding almost everywhere survives symmetrization. No measurability hypothesis on the property is necessary.
```
theorem ae_symmetrize_of_rotate_invariant (pi : Measure Triple) {P : Triple → Prop}
    (hP : ∀ᵐ t ∂pi, P t) (hrotate : ∀ t, P (rotate t) ↔ P t) :
    ∀ᵐ t ∂symmetrize pi, P t := by
…
```
Mentions: OAI.Problem356.Triple, OAI.Problem356.Cyclic.rotate, OAI.Problem356.Cyclic.symmetrize
theorem OAI.Problem356.Cyclic.averageMarginal_probability line 90
theorem OAI.Problem356.Cyclic.invDistance_comm line 96
theorem OAI.Problem356.Cyclic.cost_rotate line 99
theorem OAI.Problem356.Cyclic.cost_rotate_symm line 105
theorem OAI.Problem356.Cyclic.lintegral_symmetrize line 108