OAI/Analysis/AffineBernstein/SigmaTransform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.continuousAt_tubeLogMassWeight_fixed line 21
2. lemma OAI.AffineBernstein.sphere_sigma_density_linear_comp line 40

   Source comment

   Exact covariance of the actual weighted density integrated over all normal directions, with its transverse GL Jacobian cancelled by the sphere measure.

   lemma sphere_sigma_density_linear_comp {k d : ℕ}
       (bE : OrthonormalBasis (Fin d ⊕ Unit) ℝ E)
       (B : Space k ≃L[ℝ] Space k) (A : E ≃L[ℝ] E)
       (a : Fin k → ℝ) (ha : ∀ i, a i ≠ 0) (hBa : ∀ s i, B s i = a i*s i)
       {K : Space k → Set E} {D : Set (Space k)} (hD : IsOpen D) {s : Space k} (hsD : B s ∈ D)
       (hK : ∀ y ∈ D, IsCompact (K y)) (hne : ∀ y ∈ D, (K y).Nonempty)
       (hs : ∀ i, s i ≠ 0)
       (hH : ∀ e : E, e ≠ 0 → ContDiffAt ℝ ∞
         (fun q : Space k × E => homogeneousSupport (K q.1) q.2) (B s,e))
       (hr : ∀ e : E, e ≠ 0 → ∀ v : E, fderiv ℝ
         (fderiv ℝ (fun q : Space k × E => homogeneousSupport (K q.1) q.2)) (B s,e) (0,v) (0,e) = 0)
       (hp : ∀ e : E, e ≠ 0 → 0 < homogeneousSupport (K (B s)) e ∧
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.homogeneousSupport