OAI/Analysis/BernoulliCone/FoliationGraph.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Foliation.divergence_graph_primitive line 15
2. lemma OAI.Bernoulli.Foliation.continuous_spatial_divergence line 44
3. lemma OAI.Bernoulli.Foliation.integrated_bulk line 56

   Source documentation

   Integrating the nonlinear bulk inequality gives exactly the flux difference. This is FTC and parameter differentiation, not a postulated graph comparison.

   lemma integrated_bulk {A:E×ℝ→E} (hA:ContDiff ℝ 1 A) (x:E) {a b:ℝ} (hab:a≤b)
       (hbulk:∀s∈Icc a b,divergence (fun y:E=>A (y,s)) x+
         inner ℝ (A (x,s)) (deriv (fun t:ℝ=>A (x,t)) s)≤0) :
       2*(∫s in a..b,divergence (fun y:E=>A (y,s)) x)≤‖A (x,a)‖^2-‖A (x,b)‖^2 := by
   …

   Mentions: OAI.Bernoulli.Foliation.divergence

4. lemma OAI.Bernoulli.Foliation.divergence_smul_sub line 83
5. def OAI.Bernoulli.Foliation.graphPotential line 92
6. lemma OAI.Bernoulli.Foliation.graph_potential_identity line 94
7. lemma OAI.Bernoulli.Foliation.graph_potential_bulk_bound line 112