OAI/Analysis/AffineBernstein/WeightedChartLIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.graph_chart_weighted_affineArea_lintegral line 16

   Source comment

   Weighted local area transport. The weight is any actual function on the original graph; no integrability or measure transport premise is introduced.

   theorem graph_chart_weighted_affineArea_lintegral {E : Type*}
       [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {U Ω : Set (Space n)}
       (hU : IsOpen U) (hΩ : IsOpen Ω) {X : Space n → E} {u : Space n → ℝ}
       (hX : ContDiffOn ℝ ∞ X U) (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (a : Space n × ℝ) (L : E ≃L[ℝ] (Space n × ℝ))
       (φ : OpenPartialHomeomorph (Space n) (Space n))
       (hs : φ.source ⊆ U) (ht : φ.target ⊆ Ω)
       (hφ : ContDiffOn ℝ ∞ φ φ.source) (hψ : ContDiffOn ℝ ∞ φ.symm φ.target)
       (he : ∀ x ∈ φ.source, a+L (X x) = (φ x,u (φ x)))
       (b : Module.Basis (Fin n ⊕ Unit) ℝ E)
       {K : Set (Space n)} (hK : MeasurableSet K) (hKW : K ⊆ φ.source)
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian