Continuity of the area functional on NRR.ConvexSubbody

The real-valued area functional ConvexSubbody.area is continuous for the Hausdorff-metric topology on the fixed-parent hyperspace ConvexSubbody K. The argument proceeds through almost-everywhere convergence of the 0/1 carrier indicators and the dominated-convergence theorem, with the constant parent indicator as an integrable dominating function.

• ConvexSubbody.tendsto_indicator_ae — off the (null) frontier of the limit body, the carrier indicators converge pointwise; this holds almost everywhere.
• ConvexSubbody.tendsto_area — filter-level convergence of the areas along any convergent family of subbodies.
• ConvexSubbody.continuous_area — the area functional is continuous.

theorem NRR.ConvexSubbody.measurableSet_body {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : MeasurableSet ↑C.body

The carrier of a subbody is measurable (it is compact, hence closed).

theorem NRR.ConvexSubbody.area_eq_integral_indicator {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) : C.area = ∫ (x : Geometry.Plane), (↑C.body).indicator (fun (x : Geometry.Plane) => 1) x

Area as an indicator integral. The area of a subbody equals the Lebesgue integral of the 0/1 indicator of its carrier.

theorem NRR.ConvexSubbody.tendsto_indicator_ae {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) : ∀ᵐ (x : Geometry.Plane), Filter.Tendsto (fun (a : α) => (↑(C a).body).indicator (fun (x : Geometry.Plane) => 1) x) l (nhds ((↑C₀.body).indicator (fun (x : Geometry.Plane) => 1) x))

theorem NRR.ConvexSubbody.norm_indicator_le_parent {K : Geometry.ConvexBody Geometry.Plane} (C : ConvexSubbody K) (x : Geometry.Plane) : ‖(↑C.body).indicator (fun (x : Geometry.Plane) => 1) x‖ ≤ K.carrier.indicator (fun (x : Geometry.Plane) => 1) x

The constant parent indicator dominates every subbody indicator pointwise.

theorem NRR.ConvexSubbody.integrable_parent_indicator (K : Geometry.ConvexBody Geometry.Plane) : MeasureTheory.Integrable (fun (x : Geometry.Plane) => K.carrier.indicator (fun (x : Geometry.Plane) => 1) x) MeasureTheory.volume

The parent indicator is integrable (the parent has finite volume).

theorem NRR.ConvexSubbody.continuousAt_area {K : Geometry.ConvexBody Geometry.Plane} (C₀ : ConvexSubbody K) : ContinuousAt (fun (C : ConvexSubbody K) => C.area) C₀

Continuity at a point of the area functional, via dominated convergence with the parent indicator as dominating function.

theorem NRR.ConvexSubbody.tendsto_area {K : Geometry.ConvexBody Geometry.Plane} {α : Type u_1} {l : Filter α} {C : α → ConvexSubbody K} {C₀ : ConvexSubbody K} (hC : Filter.Tendsto C l (nhds C₀)) : Filter.Tendsto (fun (a : α) => (C a).area) l (nhds C₀.area)

Filter-level area convergence. Along any Hausdorff-convergent family of subbodies, the areas converge.

theorem NRR.ConvexSubbody.continuous_area (K : Geometry.ConvexBody Geometry.Plane) : Continuous fun (C : ConvexSubbody K) => C.area

Continuity of the area functional on the fixed-parent hyperspace.