NRR.BodySpace — lower-area subspace and the positive-area solid bridge

This module studies the closed lower-area subspace

NRR.BodySpace (K : Geometry.ConvexBody Plane) (A : ℝ) =
  {C : ConvexSubbody K // A ≤ C.area}

of the fixed-parent hyperspace ConvexSubbody K. Its elements are convex subbodies of K whose area is at least A.

• The lower-area condition is closed (continuous_area and isClosed_Ici), so BodySpace K A is a closed subtype of the compact hyperspace ConvexSubbody K, hence compact.
• When A > 0 every element has strictly positive area, so its carrier has nonempty interior and it can be repackaged as a solid geometry body Geometry.ConvexBody Plane. This solid bridge is continuous for the induced Hausdorff topology (via the named forgetful map Geometry.ConvexBody.toMathlib).
• Membership and a.e. indicator convergence lemmas are lifted from ConvexSubbody by composing with the continuous projection BodySpace.body.

@[instance_reducible]

noncomputable instance NRR.BodySpace.instMetricSpace {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} : MetricSpace (BodySpace K A)

The inherited Hausdorff metric on BodySpace K A, taken as a subtype of the hyperspace ConvexSubbody K. Because BodySpace is a def over a subtype, this instance is stated explicitly rather than inferred.

Equations

• One or more equations did not get rendered due to their size.

instance NRR.BodySpace.instT2Space {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} : T2Space (BodySpace K A)

BodySpace K A is Hausdorff (inherited from its metric).

def NRR.BodySpace.body {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (C : BodySpace K A) : ConvexSubbody K

The underlying convex subbody of an element of BodySpace K A.

Equations

• C.body = ↑C

theorem NRR.BodySpace.area_lower {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (C : BodySpace K A) : A ≤ C.body.area

The area lower bound satisfied by every element of BodySpace K A.

theorem NRR.BodySpace.continuous_body {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} : Continuous body

The projection to the underlying subbody is continuous (it is the subtype inclusion).

theorem NRR.BodySpace.isClosed_lowerArea {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} : IsClosed {C : ConvexSubbody K | A ≤ C.area}

Closedness of the lower-area condition. The locus of subbodies with area at least A is closed in the hyperspace ConvexSubbody K, since the area functional is continuous.

theorem NRR.BodySpace.isCompact_univ {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} : IsCompact Set.univ

Compactness of BodySpace K A. The whole space is compact: it is a closed subtype of the compact hyperspace ConvexSubbody K.

instance NRR.BodySpace.instCompactSpace {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} : CompactSpace (BodySpace K A)

The canonical compact-space instance on BodySpace K A.

theorem NRR.BodySpace.area_pos {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) : 0 < C.body.area

Positive area. When A > 0 every element of BodySpace K A has strictly positive area.

noncomputable def NRR.BodySpace.toGeometryConvexBody {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (C : BodySpace K A) (hA : 0 < A) : Geometry.ConvexBody Geometry.Plane

Positive-area solid bridge. When A > 0, an element of BodySpace K A repackages as a solid geometry body: its carrier is convex and compact (from the underlying subbody) and has nonempty interior (from positive area).

Equations

• C.toGeometryConvexBody hA = { carrier := ↑C.body.body, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

theorem NRR.BodySpace.toGeometryConvexBody_carrier {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (C : BodySpace K A) (hA : 0 < A) : (C.toGeometryConvexBody hA).carrier = ↑C.body.body

@[simp]

theorem NRR.BodySpace.toGeometryConvexBody_area {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (C : BodySpace K A) (hA : 0 < A) : (C.toGeometryConvexBody hA).area = C.body.area

theorem NRR.BodySpace.continuous_toGeometryConvexBody {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) : Continuous fun (C : BodySpace K A) => C.toGeometryConvexBody hA

Continuity of the solid bridge. The map sending an element of BodySpace K A to its solid geometry body is continuous for the induced Hausdorff topology on Geometry.ConvexBody Plane. By continuous_induced_rng it suffices to be continuous after the named forgetful map Geometry.ConvexBody.toMathlib, and the resulting composite is the continuous projection to the underlying root Mathlib body.

theorem NRR.BodySpace.eventually_mem_iff_of_not_mem_frontier {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {α : Type u_1} {l : Filter α} {C : α → BodySpace K A} {C₀ : BodySpace K A} (hC : Filter.Tendsto C l (nhds C₀)) {x : Geometry.Plane} (hx : x ∉ frontier ↑C₀.body.body) : ∀ᶠ (a : α) in l, x ∈ ↑(C a).body.body ↔ x ∈ ↑C₀.body.body

Frontier-complement equivalence on BodySpace K A: off the frontier of the limit body, membership in the approximating bodies eventually agrees with membership in the limit body.

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

Almost-everywhere indicator convergence on BodySpace K A: along a Hausdorff-convergent family the 0/1 carrier indicators converge pointwise almost everywhere.