OAI/Analysis/AffineBernstein/TubeDensityIntegralCompact.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.hasDerivAt_integral_tubeDensity_variation line 23

   Source comment

   The exact tube density can be differentiated under its compact integral; positivity is required only on the zero-parameter slice and is then uniform for the compactly supported variation by the tube lemma.

   lemma hasDerivAt_integral_tubeDensity_variation
       {H G : S × E → ℝ} (q₀ : S × E) (J : F →L[ℝ] (S × E))
       {W K : Set F} (hW : IsOpen W) (hK : IsCompact K) (hKW : K ⊆ W)
       (hH : ∀ x ∈ W, ContDiffAt ℝ ∞ H (q₀+J x))
       (hG : ∀ x ∈ W, ContDiffAt ℝ ∞ G (q₀+J x))
       (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (hB : ∀ x ∈ K, (tubeBaseMatrix H (q₀+J x) bS).PosDef)
       (hR : ∀ x ∈ K, (tubeRadiusMatrix H (q₀+J x) bE).PosDef) (δ : ℝ) :
       HasDerivAt (fun t : ℝ => ∫ x in K, tubeAreaDensity
         (tubeBaseMatrix (fun r => H r+t*G r) (q₀+J x) bS)
         (tubeRadiusMatrix (fun r => H r+t*G r) (q₀+J x) bE) δ ∂μ)
         (∫ x in K, tubeAreaFirstVariation (tubeBaseMatrix H (q₀+J x) bS)
   …

   Mentions: OAI.AffineBernstein.tubeBaseMatrix, OAI.AffineBernstein.tubeRadiusMatrix, OAI.AffineBernstein.tubeAreaDensity, OAI.AffineBernstein.tubeAreaFirstVariation