OAI/Geometry/HyperbolicGroups/FiniteMassTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.PlanarRecursion.pushMass line 15

   Source documentation

   Push a nonnegative mass along an actual finite map.

   def pushMass (f : A → B) (weight : A → ℝ) (b : B) : ℝ :=
   …

2. lemma OAI.HyperbolicObstruction.PlanarRecursion.pushMass_nonneg line 18
3. lemma OAI.HyperbolicObstruction.PlanarRecursion.pushMass_total line 28
4. lemma OAI.HyperbolicObstruction.PlanarRecursion.pushMass_sum line 37
5. theorem OAI.HyperbolicObstruction.PlanarRecursion.mass_le_pushMass line 50

   Source documentation

   If the image of a set lies in one dual component, its primal mass is bounded by that component's pushed-forward mass, with no injectivity of the assignment assumed or needed.

   theorem mass_le_pushMass (f : A → B) (weight : A → ℝ) (hw : ∀ a, 0 ≤ weight a)
       (U : Finset A) (C : Finset B) (hUC : ∀ a ∈ U, f a ∈ C) :
       ∑ a ∈ U, weight a ≤ ∑ b ∈ C, pushMass f weight b := by
   …

   Mentions: OAI.HyperbolicObstruction.PlanarRecursion.pushMass