OAI/Analysis/BernoulliCone/VerticalGraphLocalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Bernoulli.Foliation.real_interval_combination line 15
  2. lemma OAI.Bernoulli.Foliation.eventually_vertical_segment line 25
  3. lemma OAI.Bernoulli.Foliation.locallyLipschitz_germ line 46
  4. def OAI.Bernoulli.Foliation.verticalPotential line 56

    Source documentation

    Primitive of the actual field between two graphs; no assigned derivative.

    def verticalPotential (F:E×ℝ→E) (u v:E→ℝ) (x:E):E:=(2:ℝ) • (∫s in u x..v x,F (x,s))
  5. lemma OAI.Bernoulli.Foliation.verticalPotential_smooth_germ line 58