LocalizationFluctuationJointRestrict

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

Restricting a doubled L^2 class from the localization cube to a cell

ABK26, l.approximate.recurrence.formula, Step 2.

The missing plumbing this module supplies

Corrector.CorrectorMeasurableGradient records explicitly that "the restriction map to a subwindow. is not built here". This module builds it.

The map is the identity on representatives; the only content is that it is well defined on classes (a null set of the larger restricted measure is a null set of the smaller one) and 1-Lipschitz (eLpNorm is monotone in the measure). Neither linearity nor any Hilbert structure is used, and none is needed: measurability of a composition only asks for continuity.

Main results

• restrictHilbertBlockL2 --- the map, with coeFn_restrictHilbertBlockL2 and the compatibility restrictHilbertBlockL2_toHilbertBlockL2OfBlockField.
• lipschitzWith_restrictHilbertBlockL2, measurable_restrictHilbertBlockL2.
• measurable_toHilbertBlockL2OfBlockField_of_subset --- the transfer a consumer uses: a measurable class on the larger set gives a measurable class on the smaller one.

Binders

Only the inclusion of sets and the L^2 membership on the larger set. No estimate, no integrability, no ellipticity and no proposition about the sample law occurs.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula, Step 2.

The restriction of a doubled L^2 class

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.volumeMeasureOn_mono {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) : HCPolySupport.volumeMeasureOn T ≤ HCPolySupport.volumeMeasureOn S

The restricted volume measure is monotone in the domain.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.restrictHilbertBlockL2 {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) (f : ↥(HCPolySupport.HilbertBlockL2 S)) : ↥(HCPolySupport.HilbertBlockL2 T)

Restriction of a doubled L^2 class to a smaller domain. The identity on representatives; well defined because a null set of the larger restricted measure is a null set of the smaller one.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.restrictHilbertBlockL2 hTS f = MeasureTheory.MemLp.toLp (fun (x : HCPolySupport.Vec d) => ↑↑f x) ⋯

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.coeFn_restrictHilbertBlockL2 {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) (f : ↥(HCPolySupport.HilbertBlockL2 S)) : ↑↑(restrictHilbertBlockL2 hTS f) =ᵐ[HCPolySupport.volumeMeasureOn T] fun (x : HCPolySupport.Vec d) => ↑↑f x

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.lipschitzWith_restrictHilbertBlockL2 {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) : LipschitzWith 1 (restrictHilbertBlockL2 hTS)

The restriction map is 1-Lipschitz: eLpNorm is monotone in the measure.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.continuous_restrictHilbertBlockL2 {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) : Continuous (restrictHilbertBlockL2 hTS)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_restrictHilbertBlockL2 {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) [MeasurableSpace ↥(HCPolySupport.HilbertBlockL2 S)] [BorelSpace ↥(HCPolySupport.HilbertBlockL2 S)] [MeasurableSpace ↥(HCPolySupport.HilbertBlockL2 T)] [BorelSpace ↥(HCPolySupport.HilbertBlockL2 T)] : Measurable (restrictHilbertBlockL2 hTS)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.restrictHilbertBlockL2_toHilbertBlockL2OfBlockField {d : ℕ} {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) {F : HCPolySupport.Vec d → HCPolySupport.BlockVec d} (hS : HCPolySupport.MemBlockL2 S F) : restrictHilbertBlockL2 hTS (HCPolySupport.toHilbertBlockL2OfBlockField hS) = HCPolySupport.toHilbertBlockL2OfBlockField ⋯

Compatibility with the class map. Restricting the class of a block field is the class of the same block field on the smaller domain.

The transfer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_toHilbertBlockL2OfBlockField_of_subset {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {S T : Set (HCPolySupport.Vec d)} (hTS : T ⊆ S) [MeasurableSpace ↥(HCPolySupport.HilbertBlockL2 S)] [BorelSpace ↥(HCPolySupport.HilbertBlockL2 S)] [MeasurableSpace ↥(HCPolySupport.HilbertBlockL2 T)] [BorelSpace ↥(HCPolySupport.HilbertBlockL2 T)] {F : Omega → HCPolySupport.Vec d → HCPolySupport.BlockVec d} (hS : ∀ (omega : Omega), HCPolySupport.MemBlockL2 S (F omega)) (hmeas : Measurable fun (omega : Omega) => HCPolySupport.toHilbertBlockL2OfBlockField ⋯) : Measurable fun (omega : Omega) => HCPolySupport.toHilbertBlockL2OfBlockField ⋯

A measurable class on a larger domain restricts to a measurable class on a smaller one.