OAI/Analysis/AffineBernstein/SigmaBaseTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.continuousAt_tubeLogMassWeight line 19
2. lemma OAI.AffineBernstein.aemeasurable_tube_sigma line 43
3. lemma OAI.AffineBernstein.sigma_cell_linear_comp line 78

   Source comment

   Full base-and-normal covariance of actual sigma: positive diagonal base normalization and an arbitrary transverse GL change preserve its cell mass. The assumptions describe local regularity and convexity of the support function, not an integral bound or a transport law.

   lemma sigma_cell_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)
       {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : B '' Q ⊆ D)
       (hK : ∀ y ∈ D, IsCompact (K y)) (hne : ∀ y ∈ D, (K y).Nonempty)
       (hs : ∀ s ∈ Q, ∀ i, s i ≠ 0)
       (hH : ∀ s ∈ D, ∀ e : E, e ≠ 0 → ContDiffAt ℝ ∞
         (fun q : Space k × E => homogeneousSupport (K q.1) q.2) (s,e))
       (hr : ∀ s ∈ D, ∀ e : E, e ≠ 0 → ∀ v : E, fderiv ℝ
         (fderiv ℝ (fun q : Space k × E => homogeneousSupport (K q.1) q.2)) (s,e) (0,v) (0,e) = 0)
   …

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