CounterexampleAssembly.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem356.branchMarginal_eq_splitMeasure line 18
Source documentation
The four-map marginal is the generic finite split measure, with central weight 1/3 and four equal outer weights 1/6.
```
lemma branchMarginal_eq_splitMeasure (nu : Measure E3) (H : Fin 4 → E3 → E3) :
    branchMarginal nu (H 0) (H 1) (H 2) (H 3) =
      Splitting.splitMeasure nu (1 / 3) (fun _ : Fin 4 => 1 / 6) H := by
…
```
Mentions: OAI.Problem356.E3, OAI.Problem356.branchMarginal, OAI.Problem356.Splitting.splitMeasure

lemma OAI.Problem356.ae_branchMarginal_mem line 25

Source documentation

Support of the central measure and its four images gives support of the five-component marginal.

lemma ae_branchMarginal_mem (nu : Measure E3) {H : Fin 4 → E3 → E3}
    (hH : ∀ i, Measurable (H i)) {B U : Set E3}
    (hU : MeasurableSet U) (hfull : ∀ᵐ x ∂nu, x ∈ B)
    (hBU : B ⊆ U) (hHU : ∀ i, H i '' B ⊆ U) :
    ∀ᵐ x ∂branchMarginal nu (H 0) (H 1) (H 2) (H 3), x ∈ U := by
…

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

lemma OAI.Problem356.coulombCost_cycle_assembly line 42
lemma OAI.Problem356.triplePotential_cycle_assembly line 48
theorem OAI.Problem356.hasCoulombCounterexample_of_branches line 53

theorem OAI.Problem356.branchCoupling_optimal_of_certificate line 135

Source documentation

The concrete six-graph coupling is itself the finite optimizer. This exposes the witness used by the counterexample assembly to the separated support approximation argument.

theorem branchCoupling_optimal_of_certificate
    (nu : Measure E3) [IsProbabilityMeasure nu]
    (H : Fin 4 → E3 → E3) (hH : ∀ i, Measurable (H i))
    {U : Set E3} (hU : MeasurableSet U)
    (hmuU : ∀ᵐ x ∂branchMarginal nu (H 0) (H 1) (H 2) (H 3), x ∈ U)
    {p : E3 → ℝ≥0∞} (hp : Measurable p)
    (hpfinite : (∫⁻ x, p x ∂branchMarginal nu (H 0) (H 1) (H 2) (H 3)) ≠ ⊤)
    {C : ℝ≥0∞} (hC : C ≠ ⊤)
    (hbound : ∀ t, tripleFst t ∈ U → tripleSnd t ∈ U → tripleThd t ∈ U →
      triplePotential p t ≤ coulombCost t + C)
    (hcontact01 : ∀ᵐ x ∂nu,
      triplePotential p (x, (H 0 x, H 1 x)) = coulombCost (x, (H 0 x, H 1 x)) + C)
…

Mentions: OAI.Problem356.E3, OAI.Problem356.branchMarginal, OAI.Problem356.tripleFst, OAI.Problem356.tripleSnd, OAI.Problem356.tripleThd, OAI.Problem356.triplePotential, OAI.Problem356.coulombCost