Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.StoppingRadius

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Continuous stopping radii

This file supplies the continuous-radius ingredient for the Vitali route in the cube Calderón--Zygmund argument. The ambient Vec d carries its sup metric, so its metric closed balls are axis-parallel cubes.

theorem HCPolySupport.CubeCalderonZygmund.exists_last_crossing_of_continuousOn {E : ℝ → ℝ} {a b level : ℝ} (hab : a ≤ b) (hE : ContinuousOn E (Set.Icc a b)) (ha : level < E a) (hb : E b ≤ level) : ∃ r ∈ Set.Icc a b, E r = level ∧ ∀ s ∈ Set.Icc r b, E s ≤ level

A continuous function that starts above a level and ends below it has a last radius at the level; after that radius it stays below the level.

theorem HCPolySupport.CubeCalderonZygmund.volume_sphere_eq_zero {d : ℕ} [NeZero d] (x : Vec d) (r : ℝ) : MeasureTheory.volume (Metric.sphere x r) = 0

In positive dimension, a sup-metric sphere in Vec d has zero Lebesgue measure. This is the boundary-null fact used by dominated convergence below.

theorem HCPolySupport.CubeCalderonZygmund.continuousOn_setIntegral_closedBall {d : ℕ} [NeZero d] (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (x : Vec d) : ContinuousOn (fun (r : ℝ) => ∫ (y : Vec d) in Metric.closedBall x r, f y) (Set.Ioi 0)

The integral of an integrable function over a sup-metric closed ball is continuous as a function of its positive radius.

noncomputable def HCPolySupport.CubeCalderonZygmund.closedBallAverage {d : ℕ} (x : Vec d) (r : ℝ) (f : Vec d → ℝ) : ℝ

The normalized integral over the sup-metric ball. At positive radii this is the usual set average, since the ball has volume (2r)^d.

Equations

• HCPolySupport.CubeCalderonZygmund.closedBallAverage x r f = ((2 * r) ^ d)⁻¹ * ∫ (y : HCPolySupport.Vec d) in Metric.closedBall x r, f y

theorem HCPolySupport.CubeCalderonZygmund.closedBallAverage_eq_setAverage {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 ≤ r) (f : Vec d → ℝ) : closedBallAverage x r f = ⨍ (y : Vec d) in Metric.closedBall x r, f y

theorem HCPolySupport.CubeCalderonZygmund.continuousOn_closedBallAverage {d : ℕ} [NeZero d] (f : Vec d → ℝ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (x : Vec d) : ContinuousOn (fun (r : ℝ) => closedBallAverage x r f) (Set.Ioi 0)

Positive-radius normalized closed-ball averages of integrable data are continuous in the radius.

noncomputable def HCPolySupport.CubeCalderonZygmund.closedBallL2Energy {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] (u : Vec d → F) (x : Vec d) (r : ℝ) : ℝ

The normalized local squared energy over a sup-metric closed ball.

Equations

• HCPolySupport.CubeCalderonZygmund.closedBallL2Energy u x r = HCPolySupport.CubeCalderonZygmund.closedBallAverage x r fun (y : HCPolySupport.Vec d) => ‖u y‖ ^ 2

theorem HCPolySupport.CubeCalderonZygmund.continuousOn_closedBallL2Energy {d : ℕ} [NeZero d] {F : Type u_1} [NormedAddCommGroup F] (u : Vec d → F) (hu : MeasureTheory.Integrable (fun (y : Vec d) => ‖u y‖ ^ 2) MeasureTheory.volume) (x : Vec d) : ContinuousOn (fun (r : ℝ) => closedBallL2Energy u x r) (Set.Ioi 0)

Integrable square data has a continuous normalized local L² energy on positive radii.