OAI/Geometry/HyperbolicGroups/DipoleStepChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.sum_not_inDipole line 21

   Source documentation

   Corner-wise version of signed dipole-chain preservation. It allows the coefficient of a frozen face to be carried at one indexed corner and the coefficients of top elementary cone triangles at individual macro steps.

   lemma sum_not_inDipole {f : Perm D} {q : Perm I} {a b : I → D}
       (hF : OppositeFaces f q a b) (w : D → A) (hw : ∀ i, w (a i) + w (b i) = 0) :
       ∑ x : {x : D // ¬ InDipole a b x}, w x.val = ∑ x : D, w x := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.OppositeFaces, OAI.HyperbolicObstruction.PictureSwitch.PictureMap.InDipole