OAI/Analysis/BernoulliCone/ClampedGraphBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Foliation.gradient_eq_of_order_contact line 15
2. lemma OAI.Bernoulli.Foliation.graph_divergence_zero_contact line 26
3. lemma OAI.Bernoulli.Foliation.graph_potential_bulk_bound_open line 32
4. lemma OAI.Bernoulli.Foliation.split_graph_bound_open line 49

   Source documentation

   The clamped primitive only needs a jump condition when the seam lies strictly between the endpoint graphs. On contact sets the two gradients agree, so the spurious branch cancels exactly.

   lemma split_graph_bound_open {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:∀y,u y≤w y) (hwv:∀y,w y≤v y)
       (hbulkA:∀s∈Ioo (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∈Ioo (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:u x<w x → w x<v x → ‖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+
         ‖(if u x=w x then B else A) (x,u x)‖^2-
           2*inner ℝ ((if u x=w x then B else A) (x,u x)) (gradient u x) := by
   …

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