OAI/Analysis/BernoulliCone/FoliationSeam.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Foliation.seam_flux_identity line 13

   Source documentation

   The extended calibration jump across the graph of a matching seam.

   lemma seam_flux_identity (Gp Gm H N:E) (ρp ρm:ℝ)
       (hp:H=Gp+ρp • N) (hm:H=Gm+ρm • N) :
       ‖Gp‖^2-‖Gm‖^2-2*inner ℝ (Gp-Gm) H=
         -(ρp+ρm)*inner ℝ (Gp-Gm) N := by
   …

2. lemma OAI.Bernoulli.Foliation.seam_flux_nonpos line 32