OAI/Analysis/CoulombTransport/BranchSeparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem356.BranchSeparation.components line 15

   Source documentation

   The central compact set and its four transported copies.

   def components (K : Set E3) (H : Fin 4 → E3 → E3) : Fin 5 → Set E3 :=
   …

   Mentions: OAI.Problem356.E3

2. lemma OAI.Problem356.BranchSeparation.compact_components line 18
3. lemma OAI.Problem356.BranchSeparation.measurableSet_separated line 24
4. theorem OAI.Problem356.BranchSeparation.exists_ae_separated_branchCoupling line 37

   Source documentation

   Uniform separation for the actual cyclic two-branch coupling follows from compactness and disjointness of its five component sets.

   theorem exists_ae_separated_branchCoupling
       {nu : Measure E3} {K : Set E3} (hK : IsCompact K)
       (hnu : ∀ᵐ x ∂nu, x ∈ K) {H : Fin 4 → E3 → E3}
       (hH : ∀ i, Measurable (H i)) (hcont : ∀ i, ContinuousOn (H i) K)
       (hdisjoint : Pairwise (fun i j => Disjoint (components K H i) (components K H j))) :
       ∃ eta : ℝ, 0 < eta ∧
         ∀ᵐ t ∂branchCoupling nu (H 0) (H 1) (H 2) (H 3),
           CoulombEstimates.Separated eta t := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.BranchSeparation.components, OAI.Problem356.branchCoupling, OAI.Problem356.CoulombEstimates.Separated

5. theorem OAI.Problem356.BranchSeparation.ae_mem_branchMarginal_components line 65

   Source documentation

   The branch marginal is concentrated on the union of the central compact set and its four images.

   theorem ae_mem_branchMarginal_components
       {nu : Measure E3} {K : Set E3} (hK : IsCompact K)
       (hnu : ∀ᵐ x ∂nu, x ∈ K) {H : Fin 4 → E3 → E3}
       (hH : ∀ i, Measurable (H i)) (hcont : ∀ i, ContinuousOn (H i) K) :
       ∀ᵐ x ∂branchMarginal nu (H 0) (H 1) (H 2) (H 3),
         x ∈ ⋃ i, components K H i := by
   …

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

6. theorem OAI.Problem356.BranchSeparation.compact_support_and_separation line 91

   Source documentation

   The compact support and uniformly separated optimizer hypotheses needed for finite Monge approximation hold for the explicit branch construction.

   theorem compact_support_and_separation
       {nu : Measure E3} {K : Set E3} (hK : IsCompact K)
       (hnu : ∀ᵐ x ∂nu, x ∈ K) {H : Fin 4 → E3 → E3}
       (hH : ∀ i, Measurable (H i)) (hcont : ∀ i, ContinuousOn (H i) K)
       (hdisjoint : Pairwise (fun i j => Disjoint (components K H i) (components K H j))) :
       (∃ S : Set E3, IsCompact S ∧
         ∀ᵐ x ∂branchMarginal nu (H 0) (H 1) (H 2) (H 3), x ∈ S) ∧
       (∃ eta : ℝ, 0 < eta ∧
         ∀ᵐ t ∂branchCoupling nu (H 0) (H 1) (H 2) (H 3),
           CoulombEstimates.Separated eta t) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.BranchSeparation.components, OAI.Problem356.branchMarginal, OAI.Problem356.branchCoupling, OAI.Problem356.CoulombEstimates.Separated

7. lemma OAI.Problem356.BranchSeparation.disjoint_components_mono line 106

   Source documentation

   A compact subcomponent retains disjointness of the larger local domains.

   lemma disjoint_components_mono {K B : Set E3} (hKB : K ⊆ B)
       {H : Fin 4 → E3 → E3}
       (hB : Pairwise (fun i j => Disjoint (components B H i) (components B H j))) :
       Pairwise (fun i j => Disjoint (components K H i) (components K H j)) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.BranchSeparation.components

8. theorem OAI.Problem356.BranchSeparation.finite_cost_branchCoupling line 118

   Source documentation

   Under the compact disjoint-component hypotheses, the explicit candidate already has finite cost, before applying any dual certificate.

   theorem finite_cost_branchCoupling
       {nu : Measure E3} [IsProbabilityMeasure nu] {K : Set E3} (hK : IsCompact K)
       (hnu : ∀ᵐ x ∂nu, x ∈ K) {H : Fin 4 → E3 → E3}
       (hH : ∀ i, Measurable (H i)) (hcont : ∀ i, ContinuousOn (H i) K)
       (hdisjoint : Pairwise (fun i j => Disjoint (components K H i) (components K H j))) :
       (∫⁻ t, coulombCost t ∂branchCoupling nu (H 0) (H 1) (H 2) (H 3)) < ⊤ := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.BranchSeparation.components, OAI.Problem356.coulombCost, OAI.Problem356.branchCoupling