OAI/Analysis/AffineBernstein/SupportVariation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.flatNormalProjection line 18

   Source comment

   Homogeneous extension of an actual test function off the affine normal chart.

   def flatNormalProjection (ℓ : E →L[ℝ] ℝ) (q₀ : S × E)
       (C : (S × E) →L[ℝ] F) (q : S × E) : F :=
   …

2. def OAI.AffineBernstein.flatSupportVariation line 22
3. def OAI.AffineBernstein.supportGradient line 26
4. lemma OAI.AffineBernstein.contDiffAt_flatNormalProjection line 30
5. lemma OAI.AffineBernstein.contDiffAt_flatSupportVariation line 38
6. lemma OAI.AffineBernstein.contDiffAt_supportGradient line 45
7. lemma OAI.AffineBernstein.supportGradient_angular line 50
8. lemma OAI.AffineBernstein.flatNormalProjection_smul line 61
9. lemma OAI.AffineBernstein.flatSupportVariation_smul line 70
10. lemma OAI.AffineBernstein.flatSupportVariation_euler line 76
11. lemma OAI.AffineBernstein.flatNormalProjection_on_chart line 101
12. lemma OAI.AffineBernstein.flatSupportVariation_on_chart line 113
13. lemma OAI.AffineBernstein.supportGradient_flatVariation_eq_zero line 120
14. lemma OAI.AffineBernstein.tsupport_flatSupportVelocity_subset line 144
15. lemma OAI.AffineBernstein.contDiff_flatSupportVelocity line 156