OAI/Geometry/ProjectionBody/BrightnessSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.real_measure_image_halfspaceBody line 18

   Source documentation

   Convert the genuine facet-measure sum to the balanced absolute-slope formula. Every geometric input, including each projected facet measure, remains explicit.

   theorem real_measure_image_halfspaceBody
       (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ) (q : V →ₗ[ℝ] W) (μ : Measure W)
       {u : V} (hqu : q u = 0) (hu : ∃ i, 0 < a i u)
       (hker : LinearMap.ker q = Submodule.span ℝ {u})
       (hmeas : ∀ i, MeasurableSet (q '' boundingFace a b i))
       (hnull : ∀ i j, i ≠ j →
         μ (q '' (boundingFace a b i ∩ boundingFace a b j)) = 0)
       (c : ℝ) (hc : 0 ≤ c) (hbalance : ∑ i, a i u = 0)
       (hfacet : ∀ i, μ (q '' boundingFace a b i) = ENNReal.ofReal (c * |a i u|)) :
       (μ (q '' halfspaceBody a b)).toReal = c * (∑ i, |a i u|) / 2 := by
   …

   Mentions: OAI.ProjectionCounterexample.boundingFace, OAI.ProjectionCounterexample.halfspaceBody