ProductPlan.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem356.isThreeCoupling_prod line 13
Source documentation
The independent triple is always an admissible coupling of a probability.
```
theorem isThreeCoupling_prod (mu : Measure E3) [IsProbabilityMeasure mu] :
    IsThreeCoupling mu (mu.prod (mu.prod mu)) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.IsThreeCoupling
theorem OAI.Problem356.measurable_pairInteraction line 26
Source documentation
The Coulomb pair interaction is measurable, including its infinite diagonal.
```
private theorem measurable_pairInteraction :
    Measurable (fun p : E3 × E3 => invDistance p.1 p.2) := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.invDistance
theorem OAI.Problem356.map_pair_fst_snd_prod line 31
theorem OAI.Problem356.map_pair_fst_thd_prod line 38
theorem OAI.Problem356.lintegral_three_pairs_prod line 45
def OAI.Problem356.coulombPairEnergy line 65
Source documentation
The pair interaction energy of an independently sampled pair.
```
def coulombPairEnergy (mu : Measure E3) : ℝ≥0∞ :=
…
```
Mentions: OAI.Problem356.E3
theorem OAI.Problem356.lintegral_coulombCost_prod line 68
theorem OAI.Problem356.kantorovichValue_le_three_pairEnergy line 72
theorem OAI.Problem356.kantorovichValue_lt_top_of_pairEnergy_lt_top line 79