FacetMeasure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ProjectionCounterexample.measure_image_halfspaceBody_eq_sum_visible line 18

Source documentation

Finite additivity for shadows of visible faces. The geometric hypotheses are explicit: the later applications must prove measurability and nullity of the projected intersections. No facet-volume formula is assumed here.

theorem measure_image_halfspaceBody_eq_sum_visible
    (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) :
    μ (q '' halfspaceBody a b) =
      ∑ i : {i : ι // 0 < a i u}, μ (q '' boundingFace a b i.1) := by
…

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