OAI/Analysis/CoulombTransport/BranchOptimizer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem356.branchOptimizer_cost_cycle line 12
2. lemma OAI.Problem356.branchOptimizer_potential_cycle line 18
3. theorem OAI.Problem356.branchCoupling_optimality_of_shifted_certificate line 26

   Source documentation

   The explicit six-graph branch coupling is itself a finite optimizer. This preserves the identity of the optimizer, unlike an existential attainment statement, so its geometric separation can be used in Monge approximation.

   theorem branchCoupling_optimality_of_shifted_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

4. theorem OAI.Problem356.branchCoupling_optimality_of_real_certificate line 60

   Source documentation

   Signed-potential version of explicit branch optimizer certification. The assumptions are a subset of the real counterexample assembly assumptions; no density, injectivity, or nonattainment hypothesis is required.

   theorem branchCoupling_optimality_of_real_certificate
       (nu : Measure E3) [IsProbabilityMeasure nu]
       (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)
       {u : E3 → ℝ} (hu : Measurable u) {M : ℝ} (hM : 0 ≤ M)
       (hubound : ∀ x ∈ U, -M ≤ u x ∧ u x ≤ M)
       (hbound : ∀ t, tripleFst t ∈ U → tripleSnd t ∈ U → tripleThd t ∈ U →
         ENNReal.ofReal (u (tripleFst t) + u (tripleSnd t) + u (tripleThd t)) ≤
           coulombCost t)
       (hcontact01 : ∀ᵐ x ∂nu,
   …

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