PiecewiseFoliationGraph.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Bernoulli.Foliation.divergence_add line 15
lemma OAI.Bernoulli.Foliation.graphPotential_differentiableAt line 22
def OAI.Bernoulli.Foliation.splitGraphPotential line 31

theorem OAI.Bernoulli.Foliation.split_graph_bound line 36

Source documentation

The moving seam contribution is derived from the two actual graph primitives. The sign is exactly the extended calibration flux jump.

theorem split_graph_bound {A B:E×ℝ→E} (hA:ContDiff ℝ 1 A) (hB:ContDiff ℝ 1 B)
    {u w v:E→ℝ} {x:E} (hu:DifferentiableAt ℝ u x) (hw:DifferentiableAt ℝ w x)
    (hv:DifferentiableAt ℝ v x) (huw:u x≤w x) (hwv:w x≤v x)
    (hbulkA:∀s∈Icc (u x) (w x),divergence (fun y:E=>A (y,s)) x+
      inner ℝ (A (x,s)) (deriv (fun t:ℝ=>A (x,t)) s)≤0)
    (hbulkB:∀s∈Icc (w x) (v x),divergence (fun y:E=>B (y,s)) x+
      inner ℝ (B (x,s)) (deriv (fun t:ℝ=>B (x,t)) s)≤0)
    (hjump:‖B (x,w x)‖^2-‖A (x,w x)‖^2-
      2*inner ℝ (B (x,w x)-A (x,w x)) (gradient w x)≤0) :
    divergence (splitGraphPotential A B u w v) x≤‖gradient v x‖^2+
      ‖A (x,u x)‖^2-2*inner ℝ (A (x,u x)) (gradient u x) := by
…

Mentions: OAI.Bernoulli.Foliation.divergence, OAI.Bernoulli.Foliation.splitGraphPotential