OAI/Analysis/BernoulliCone/CompactLipschitzDivergence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Foliation.locallyLipschitz_compact_lipschitz line 16
2. lemma OAI.Bernoulli.Foliation.integral_directional_compact line 59
3. lemma OAI.Bernoulli.Foliation.integrable_directional_compact line 81
4. lemma OAI.Bernoulli.Foliation.integrable_divergence_compact line 93
5. lemma OAI.Bernoulli.Foliation.divergence_zero_outside_support line 114
6. theorem OAI.Bernoulli.Foliation.integral_divergence_compact line 122

   Source documentation

   The divergence of a genuine compactly supported Lipschitz vector field has integral zero, with the a.e. derivative justified by Rademacher.

   theorem integral_divergence_compact {d:ℕ} {F:Space d→Space d} {K:ℝ≥0}
       (hF:LipschitzWith K F) (hc:HasCompactSupport F) :
       (∫x,divergence F x)=0 := by
   …

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