OAI/Analysis/CoulombTransport/IsometryTransport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem356.IsometryTransport.lift line 13

   Source documentation

   Apply the same spatial isometry to each particle.

   def lift (e : E3 ≃ᵢ E3) : Triple ≃ᵐ Triple :=
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.Triple

2. theorem OAI.Problem356.IsometryTransport.lift_apply line 17
3. theorem OAI.Problem356.IsometryTransport.invDistance_apply line 20
4. theorem OAI.Problem356.IsometryTransport.cost_lift line 24
5. theorem OAI.Problem356.IsometryTransport.lintegral_map_lift line 29
6. theorem OAI.Problem356.IsometryTransport.coupling_map_lift line 34
7. theorem OAI.Problem356.IsometryTransport.kantorovichValue_map_le line 49
8. theorem OAI.Problem356.IsometryTransport.kantorovichValue_map line 58
9. theorem OAI.Problem356.IsometryTransport.supporting_inequality_image line 66

   Source documentation

   Transport a bounded-domain supporting potential without changing the cost.

   theorem supporting_inequality_image (e : E3 ≃ᵢ E3) (U : Set E3) (u : E3 → ℝ)
       (h : ∀ x ∈ U, ∀ y ∈ U, ∀ z ∈ U,
         ENNReal.ofReal (u x + u y + u z) ≤ coulombCost (x, (y, z))) :
       ∀ x ∈ e '' U, ∀ y ∈ e '' U, ∀ z ∈ e '' U,
         ENNReal.ofReal (u (e.symm x) + u (e.symm y) + u (e.symm z)) ≤
           coulombCost (x, (y, z)) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.coulombCost

10. theorem OAI.Problem356.IsometryTransport.supporting_equality_image line 78
11. theorem OAI.Problem356.IsometryTransport.map_densityMeasure line 87

    Source documentation

    Orthogonal changes of variables transport a density without a Jacobian factor.

    theorem map_densityMeasure (e : E3 ≃ₗᵢ[ℝ] E3) (rho : E3 → ℝ)
        (hrho : Measurable rho) :
        Measure.map e (densityMeasure rho) = densityMeasure (fun x => rho (e.symm x)) := by
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.densityMeasure

12. theorem OAI.Problem356.IsometryTransport.smoothDensity_comp_symm line 100
13. def OAI.Problem356.IsometryTransport.axisSwap line 111

    Source documentation

    Exchange the first and second Euclidean axes, leaving the third fixed.

    def axisSwap : E3 ≃ₗᵢ[ℝ] E3 :=
    …

    Mentions: OAI.Problem356.E3

14. theorem OAI.Problem356.IsometryTransport.axisSwap_single line 114
15. theorem OAI.Problem356.IsometryTransport.axisSwap_zero line 118
16. theorem OAI.Problem356.IsometryTransport.axisSwap_first line 120
17. theorem OAI.Problem356.IsometryTransport.axisSwap_second line 124