OAI/Analysis/BernoulliCone/FoliationDifferential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.Foliation.spatialGradient line 16

   Source documentation

   Spatial gradient of a smooth one-parameter family, as a joint field.

   def spatialGradient (F:E×ℝ→ℝ) (p:E×ℝ) : E :=
   …

2. def OAI.Bernoulli.Foliation.divergence line 19
3. lemma OAI.Bernoulli.Foliation.inner_spatialGradient line 22
4. lemma OAI.Bernoulli.Foliation.linear_prod_decomposition line 28
5. lemma OAI.Bernoulli.Foliation.sliceLeft_hasFDerivAt line 35
6. lemma OAI.Bernoulli.Foliation.spatialGradient_eq line 43
7. lemma OAI.Bernoulli.Foliation.spatialGradient_contDiffAt line 52
8. lemma OAI.Bernoulli.Foliation.parameter_directional line 58
9. lemma OAI.Bernoulli.Foliation.divergence_gradient line 75
10. lemma OAI.Bernoulli.Foliation.foliation_divergence line 101

    Source documentation

    Cancellation of the parameter derivatives in the extended calibration. This is the differential identity for an actual foliation, not an assumed PDE.

    lemma foliation_divergence {F:E×ℝ→ℝ} {L:E×ℝ→ℝ} {p:E×ℝ}
        (hF:ContDiffAt ℝ ∞ F (p.1,L p)) (hL:ContDiffAt ℝ ∞ L p)
        (he:∀ᶠ z in 𝓝 p,F (z.1,L z)=z.2)
        (hρ:fderiv ℝ F (p.1,L p) (0,1)≠0) :
        let A:E×ℝ→E:=fun z=>spatialGradient F (z.1,L z)
    …

    Mentions: OAI.Bernoulli.Foliation.spatialGradient