SolutionSelector

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The selected solution, the closed cube, and evaluation by ball averages

Three deterministic ingredients of the measurability of the localized quantities.

The selected solution. The rough-field Dirichlet problem on y + □_n has a solution for every sample and every Hölder forcing field; solutionAt names one, and by the almost-everywhere uniqueness of the problem any other choice differs from it on a null set only, so every quantity built from its continuous representative is independent of the choice.

The closed cube. The coefficient field is measured in the supremum norm on a compact set; closedCubeAt y n is the closed cube of side 3^n centred at y, which contains y + □_n, is compact, and sits inside a centred open cube of large enough scale. clampTo is the coordinatewise retraction onto it.

Evaluation by ball averages. A function continuous on an open set is the limit of its averages over shrinking balls, and averages depend only on the almost-everywhere class. This is what turns pointwise evaluation of a continuous representative into a countable limit of integrals of the H¹ witness.

References

• ABK26, the localized Dirichlet problems of Section 5.1.

1. The selected solution

noncomputable def Algsuperdiff.Section5.Support.solutionAt {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) : HCPolySupport.H1Function (cubeSetAt y n)

A solution of the rough-field Dirichlet problem on y + □_n.

The solution is obtained by choice from an existence statement whose input includes the bound Kg, although Kg does not constrain the solution: two admissible bounds for the same forcing field may name syntactically different solutions. Every consumer must therefore pass through the almost-everywhere uniqueness of the Dirichlet solution, never through equality of selections.

Equations

• Algsuperdiff.Section5.Support.solutionAt M m n y omega hg = ⋯.choose

theorem Algsuperdiff.Section5.Support.isDirichletSolutionAt_solutionAt {d : ℕ} (M : Section3.ABKModel d) (m n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {Kg : ℝ} (hg : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) Kg g) : IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu m omega).toCoeffField y n (solutionAt M m n y omega hg) g

2. The closed cube

def Algsuperdiff.Section5.Support.closedCubeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : Set (HCPolySupport.Vec d)

The closed cube of side 3^n centred at y.

Equations

• Algsuperdiff.Section5.Support.closedCubeAt y n = {x : HCPolySupport.Vec d | ∀ (i : Fin d), |x i - y i| ≤ 1 / 2 * 3 ^ n}

theorem Algsuperdiff.Section5.Support.cubeSetAt_subset_closedCubeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : cubeSetAt y n ⊆ closedCubeAt y n

theorem Algsuperdiff.Section5.Support.isClosed_closedCubeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : IsClosed (closedCubeAt y n)

theorem Algsuperdiff.Section5.Support.isBounded_closedCubeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : Bornology.IsBounded (closedCubeAt y n)

theorem Algsuperdiff.Section5.Support.isCompact_closedCubeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : IsCompact (closedCubeAt y n)

instance Algsuperdiff.Section5.Support.compactSpace_closedCubeAt {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : CompactSpace ↑(closedCubeAt y n)

theorem Algsuperdiff.Section5.Support.exists_closedCubeAt_subset_openCubeSet {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : ∃ (ell : ℤ), closedCubeAt y n ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)

noncomputable def Algsuperdiff.Section5.Support.clampTo {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : HCPolySupport.Vec d

The coordinatewise retraction onto the closed cube.

Equations

• Algsuperdiff.Section5.Support.clampTo y n x i = max (y i - 1 / 2 * 3 ^ n) (min (x i) (y i + 1 / 2 * 3 ^ n))

theorem Algsuperdiff.Section5.Support.continuous_clampTo {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) : Continuous (clampTo y n)

theorem Algsuperdiff.Section5.Support.clampTo_mem {d : ℕ} (y : HCPolySupport.Vec d) (n : ℤ) (x : HCPolySupport.Vec d) : clampTo y n x ∈ closedCubeAt y n

theorem Algsuperdiff.Section5.Support.clampTo_eq_self {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ closedCubeAt y n) : clampTo y n x = x

3. Evaluation by ball averages

theorem Algsuperdiff.Section5.Support.tendsto_setAverage_ball_of_continuousOn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : IsOpen U) {f : HCPolySupport.Vec d → ℝ} (hcont : ContinuousOn f U) {x : HCPolySupport.Vec d} (hx : x ∈ U) {r : ℕ → ℝ} (hrpos : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => ⨍ (z : HCPolySupport.Vec d) in Metric.ball x (r k), f z) Filter.atTop (nhds (f x))

A function continuous on an open set is the limit of its averages over shrinking balls centred at a point of the set.