LocalizationFluctuationJointComponents

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

Assembling a doubled L^2 class from its two vector legs

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

Why this module exists

The measurability hypothesis of LocalizationFluctuationJointField is stated at the doubled carrier HilbertBlockL2. This module is the bridge.

Method

The pairing map is not treated as a bilinear object at all. Writing

  (F, G) = iota_1 F + iota_2 G ,

with iota_1 v = (v, 0) and iota_2 v = (0, v), each summand is post-composition of an L^2 class with a fixed continuous linear map of the fibres, i.e. ContinuousLinearMap.compLpL, which is itself a continuous linear map of L^2 spaces. Continuity of the assembly is therefore free, and no eLpNorm computation occurs anywhere below.

Main results

• measurable_toHilbertBlockL2OfComponents --- a measurable class for each leg gives a measurable doubled class.
• toHilbertBlockL2OfBlockField_const --- the constant leg (the load P_z of e.Pz.def) is the image of its block vector under the continuous linear blockVecToHilbertBlockL2Const.

Binders

Beyond the typing binders: the vector-L^2 memberships of the two legs and measurability of their classes. No estimate, no integrability 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, e.Pz.def, e.Fz.def.

The two fibre embeddings

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.hilbertBlockInl (d : ℕ) : HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertBlockVec d

The potential-leg embedding of a Hilbert vector into a Hilbert block vector.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.hilbertBlockInr (d : ℕ) : HCPolySupport.HilbertVec d →L[ℝ] HCPolySupport.HilbertBlockVec d

The flux-leg embedding of a Hilbert vector into a Hilbert block vector.

Equations

• One or more equations did not get rendered due to their size.

Assembling the doubled class

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.toHilbertBlockL2OfComponents_eq_compLp_add {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 U f) (hg : HCPolySupport.MemVectorL2 U g) : HCPolySupport.toHilbertBlockL2OfComponents hf hg = (hilbertBlockInl d).compLp (HCPolySupport.toHilbertVectorL2OfVecField hf) + (hilbertBlockInr d).compLp (HCPolySupport.toHilbertVectorL2OfVecField hg)

The doubled class of a pair of vector fields is the sum of the two post-composed vector classes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_toHilbertBlockL2OfComponents {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {U : Set (HCPolySupport.Vec d)} [MeasurableSpace ↥(HCPolySupport.HilbertVectorL2 U)] [BorelSpace ↥(HCPolySupport.HilbertVectorL2 U)] [MeasurableSpace ↥(HCPolySupport.HilbertBlockL2 U)] [BorelSpace ↥(HCPolySupport.HilbertBlockL2 U)] [SecondCountableTopology ↥(HCPolySupport.HilbertBlockL2 U)] {f g : Omega → HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : ∀ (omega : Omega), HCPolySupport.MemVectorL2 U (f omega)) (hg : ∀ (omega : Omega), HCPolySupport.MemVectorL2 U (g omega)) (hfm : Measurable fun (omega : Omega) => HCPolySupport.toHilbertVectorL2OfVecField ⋯) (hgm : Measurable fun (omega : Omega) => HCPolySupport.toHilbertVectorL2OfVecField ⋯) : Measurable fun (omega : Omega) => HCPolySupport.toHilbertBlockL2OfComponents ⋯ ⋯

A measurable class for each leg gives a measurable doubled class.

The constant leg

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.toHilbertBlockL2OfBlockField_const {d : ℕ} {U : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn U)] (P : HCPolySupport.BlockVec d) (hP : HCPolySupport.MemBlockL2 U fun (x : HCPolySupport.Vec d) => P) : HCPolySupport.toHilbertBlockL2OfBlockField hP = HCPolySupport.blockVecToHilbertBlockL2Const P

The doubled class of a constant block field is its image under the proved continuous linear constant embedding.