High-contrast homogenization: Provider.Response.CutoffCubeAverage

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Reference-cube normalization for the adapted cutoff

The canonical product cutoff is one on its inner cube. This file records the corresponding lower bound on its cube average for arbitrary radii, and chooses dimension-dependent radii whose inner cube occupies at least half the volume.

theorem HCPolySupport.HighContrast.Response.volume_scaledOpenCubeSet_toReal {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ : 0 ≤ ρ) : (MeasureTheory.volume (scaledOpenCubeSet Q ρ)).toReal = (ρ * cubeScaleFactor Q) ^ d

The volume of the concentric open subcube is its relative side length to the power of the dimension, times the volume scale of the parent cube.

theorem HCPolySupport.HighContrast.Response.innerRatio_pow_le_cubeAverage_canonicalFun {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hρ₁_lt_one : ρ₁ < 1) : ρ₁ ^ d ≤ cubeAverage Q (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)

The canonical product cutoff has average at least the relative volume of the inner cube.

theorem HCPolySupport.HighContrast.Response.half_le_innerRatio_pow (d : ℕ) [NeZero d] : 1 / 2 ≤ (1 - 1 / (2 * ↑d)) ^ d

Bernoulli's inequality shows that the chosen inner side ratio occupies at least half the volume in every positive dimension.

theorem HCPolySupport.HighContrast.Response.cutoffRadii_spec (d : ℕ) [NeZero d] : 0 < 1 - 1 / (2 * ↑d) ∧ 1 - 1 / (2 * ↑d) < 1 - 1 / (4 * ↑d) ∧ 1 - 1 / (4 * ↑d) < 1

The selected inner and outer relative radii are strictly ordered inside the parent cube.