theorem outer_radius_pos_of_positive_measure {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hdim : 0 < Module.finrank ℝ E) {Q : Set E} {xStar : E} {D : ℝ} (hxStar : xStar ∈ Q) (hQ_pos : 0 < μ.real Q) (hQ_subset : Q ⊆ Metric.closedBall xStar D) : 0 < D

Helper for Theorem 3.51: if a positive-volume set Q contains the center xStar and is contained in Metric.closedBall xStar D, then the outer radius D must be positive.

theorem comparison_set_contains_domain_of_outer_radius_lt {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Q Sk : Set E} {xStar : E} {D vkStar : ℝ} (hQ_subset : Q ⊆ Metric.closedBall xStar D) (hball : Metric.closedBall xStar vkStar ∩ Q ⊆ Sk) (hDv : D < vkStar) : Q ⊆ Sk

Helper for Theorem 3.51: if the inner radius strictly exceeds the outer one, then the inclusion hypothesis already forces Q ⊆ Sk.

theorem homothety_image_subset_closedBall_inter_of_convex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Q : Set E} {xStar : E} {α D : ℝ} (hα0 : 0 ≤ α) (hα1 : α ≤ 1) (hQ_convex : Convex ℝ Q) (hxStar : xStar ∈ Q) (hQ_subset : Q ⊆ Metric.closedBall xStar D) : ⇑(AffineMap.homothety xStar α) '' Q ⊆ Metric.closedBall xStar (α * D) ∩ Q

Helper for Theorem 3.51: the homothety of Q centered at xStar with factor α ∈ [0, 1] stays inside the smaller closed ball and inside Q itself.

theorem measureReal_homothety_image {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Q : Set E} {xStar : E} {α : ℝ} (hα0 : 0 ≤ α) : μ.real (⇑(AffineMap.homothety xStar α) '' Q) = α ^ Module.finrank ℝ E * μ.real Q

Helper for Theorem 3.51: the real-valued Haar measure of a homothety image scales by α ^ dim when α ≥ 0.

theorem alpha_le_volume_ratio_rpow_of_measure_bound {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hdim : 0 < Module.finrank ℝ E) {Q Sk : Set E} {α : ℝ} (hQ_pos : 0 < μ.real Q) (hα0 : 0 ≤ α) (hmeasure : α ^ Module.finrank ℝ E * μ.real Q ≤ μ.real Sk) : α ≤ (μ.real Sk / μ.real Q).rpow (1 / ↑(Module.finrank ℝ E))

Helper for Theorem 3.51: a lower bound on α ^ dim * μ.real Q turns into the claimed dim-th-root bound on α.

theorem inner_ball_radius_le_outer_radius_mul_volume_ratio_rpow_of_convex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hdim : 0 < Module.finrank ℝ E) {Q Sk : Set E} {xStar : E} {D vkStar : ℝ} (hQ_convex : Convex ℝ Q) (hxStar : xStar ∈ Q) (hQ_pos : 0 < μ.real Q) (hD_pos : 0 < D) (hvkStar_le : vkStar ≤ D) (hQ_subset : Q ⊆ Metric.closedBall xStar D) (hSk_meas : MeasurableSet Sk) (hSk_subset : Sk ⊆ Q) (hball : Metric.closedBall xStar vkStar ∩ Q ⊆ Sk) : vkStar ≤ D * (μ.real Sk / μ.real Q).rpow (1 / ↑(Module.finrank ℝ E))

Theorem 3.51, stated at the intrinsic owner level: if 0 < Module.finrank ℝ E, if a convex set Q of positive μ-volume in a finite-dimensional real normed space is contained in the closed ball B(xStar, D) with 0 < D, if Sk ⊆ Q is measurable, and if B(xStar, vkStar) ∩ Q ⊆ Sk, then under the chapter's standing center context xStar ∈ Q and the standing radius bound vkStar ≤ D coming from the earlier localization setup, the inner radius vkStar is bounded by D times the dim-th root of the Haar-measure ratio μ.real Sk / μ.real Q. The finite-volume side condition on Sk is derived internally from Sk ⊆ Q ⊆ B(xStar, D). Specializing to the canonical choice μ = Measure.addHaar gives the chapter owner used downstream, and in Euclidean space this differs from textbook Lebesgue volume only by a global positive normalization factor, so the displayed ratio is unchanged.