OAI/Analysis/AffineBernstein/EuclideanChain.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.continuousLinearMap_euclidean_sum line 13
2. lemma OAI.AffineBernstein.euclidean_chain_fderiv line 21
3. def OAI.AffineBernstein.euclideanGradientSquare line 39

   Source comment

   Euclidean norm squared of the gradient, written in the fixed orthonormal coordinate basis.

   def euclideanGradientSquare {k : ℕ} (φ : Space k → ℝ) (s : Space k) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

4. lemma OAI.AffineBernstein.euclideanGradientSquare_eq_norm line 42
5. lemma OAI.AffineBernstein.euclideanGradientSquare_nonneg line 48
6. lemma OAI.AffineBernstein.euclideanGradientSquare_zero line 51
7. lemma OAI.AffineBernstein.tsupport_euclideanGradientSquare line 55
8. lemma OAI.AffineBernstein.contDiff_euclideanGradientSquare line 62
9. lemma OAI.AffineBernstein.compactSupport_euclideanGradientSquare line 66
10. lemma OAI.AffineBernstein.logPullback_gradient_nonneg line 70
11. lemma OAI.AffineBernstein.logPullback_gradient_support line 77
12. lemma OAI.AffineBernstein.logPullback_fderiv_chain line 82