LocalizedMeasurable

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

The data-side energy estimate, and measurability of the events from that of E and X

Two things.

The data-side estimate. For a fixed coefficient field the solution depends on the forcing field Lipschitz-continuously in the energy norm: subtracting the two weak equations and testing with the difference gives

  ‖∇(u_g − u_{g'})‖_{L²} ≤ lam⁻¹ d ‖g − g'‖_{L²} .

This is the linearity input of the countable-subclass reduction.

The events. The good cube event, the event Q and the percolation scale are measurable as soon as the localized error and the localized regularity are measurable functions of the sample. This isolates the one remaining input: the reduction of the suprema over the normalized forcing class to a countable subclass.

Main results

• sqrt_energy_grad_sub_le_data.
• measurableSet_goodCubeEvent_of_measurable, measurableSet_qEvent_of_measurable, measurable_percolationScaleTotal_of_measurable.

References

• ABK26, the localized quantities and the chains of good cubes of Section 5.

1. The data-side energy estimate

theorem Algsuperdiff.Section5.Support.sqrt_energy_grad_sub_le_data {d : ℕ} {y : HCPolySupport.Vec d} {n : ℤ} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (cubeSetAt y n) a) {u u' : HCPolySupport.H1Function (cubeSetAt y n)} {g g' : HCPolySupport.Vec d → HCPolySupport.Vec d} (hgL2 : HCPolySupport.MemVectorL2 (cubeSetAt y n) g) (hg'L2 : HCPolySupport.MemVectorL2 (cubeSetAt y n) g') (hu : IsDirichletSolutionAt a y n u g) (hu' : IsDirichletSolutionAt a y n u' g') : √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖u.grad x - u'.grad x‖ ^ 2) ≤ lam⁻¹ * ↑d * √(∫ (x : HCPolySupport.Vec d) in cubeSetAt y n, ‖g x - g' x‖ ^ 2)

The solution depends on the forcing field Lipschitz-continuously in the energy norm, with the dimensional factor of the supremum-norm carrier.

2. The events, from the measurability of the localized quantities

theorem Algsuperdiff.Section5.Support.measurableSet_goodCubeEvent_of_measurable {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) (n : ℤ) (y : HCPolySupport.Vec d) (ep : ℝ) (hE : Measurable (localizedError M n y)) (hX : Measurable (localizedRegularity M n y)) : MeasurableSet (goodCubeEvent M Creg n y ep)

theorem Algsuperdiff.Section5.Support.measurableSet_qEvent_of_measurable {d : ℕ} (M : Section3.ABKModel d) (Creg Cinj : ℝ) (n : ℤ) (z : HCPolySupport.Vec d) (ep : ℝ) (hE : Measurable (localizedError M n z)) (hX : Measurable (localizedRegularity M n z)) : MeasurableSet (qEvent M Creg Cinj n z ep)

theorem Algsuperdiff.Section5.Support.measurable_percolationScaleTotal_of_measurable {d : ℕ} (M : Section3.ABKModel d) (Creg Cinj : ℝ) (m : ℤ) (ep : ℝ) (hE : ∀ (n : ℤ) (z : HCPolySupport.Vec d), Measurable (localizedError M n z)) (hX : ∀ (n : ℤ) (z : HCPolySupport.Vec d), Measurable (localizedRegularity M n z)) : Measurable (percolationScaleTotal M Creg Cinj m ep)

The percolation scale is measurable as soon as the localized quantities are. This replaces the event-level hypothesis by the structural one.