OAI/Analysis/AffineBernstein/ProjectiveInverseWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.homogeneous_fiber_fderiv_scale line 18
2. lemma OAI.AffineBernstein.homogeneous_supportConormal_scale line 40
3. lemma OAI.AffineBernstein.homogeneous_inverseMetricWeight_scale line 59

   Source comment

   The conormal norm exactly cancels inverse-B homogeneity. Thus this is a well-defined weight on rays, not a coordinate-dependent flat-chart weight.

   lemma homogeneous_inverseMetricWeight_scale {K : S → Set E} {s : S} {e : E}
       {D : Set S} (hD : IsOpen D) (hs : s ∈ D)
       (hK : ∀ y ∈ D, IsCompact (K y)) (hne : ∀ y ∈ D, (K y).Nonempty)
       {c : ℝ} (hc : 0 < c)
       (hH : ContDiffAt ℝ ∞ (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,e))
       (hHc : ContDiffAt ℝ ∞ (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,c • e))
       (bS : Module.Basis ι ℝ S)
       (hB : (tubeBaseMatrix (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,e) bS).det ≠ 0)
       (v w : ι → ℝ) :
       let H := fun q : S × E => homogeneousSupport (K q.1) q.2
   …

   Mentions: OAI.AffineBernstein.homogeneousSupport, OAI.AffineBernstein.tubeBaseMatrix