Measurable stream coefficients

Coefficient-field evaluations depend measurably on the environment. Ported from the Apache-2.0 Superdiffusion source at 7f20476385d4af418f110303085ad0740c9eba46.

theorem Algsuperdiff.Section5.Measurability.measurable_streamField_apply {d : ℕ} {gamma : ℝ} (x : HCPolySupport.Vec d) : Measurable fun (omega : Field.FullSample d gamma) => Field.streamField omega x

theorem Algsuperdiff.Section5.Measurability.measurable_streamCoefficient_apply {d : ℕ} {gamma nu : ℝ} (x : HCPolySupport.Vec d) : Measurable fun (omega : Field.FullSample d gamma) => Field.streamCoefficient nu omega x

theorem Algsuperdiff.Section5.Measurability.measurable_streamCoefficient_joint {d : ℕ} {gamma nu : ℝ} : Measurable fun (p : Field.FullSample d gamma × HCPolySupport.Vec d) => Field.streamCoefficient nu p.1 p.2

noncomputable def Algsuperdiff.Section5.Measurability.streamCoefficientRestrict {d : ℕ} {gamma : ℝ} (nu : ℝ) (K : Set (HCPolySupport.Vec d)) (omega : Field.FullSample d gamma) : C(↑K, HCPolySupport.Mat d)

The full stream coefficient restricted to a compact spatial carrier.

Equations

• Algsuperdiff.Section5.Measurability.streamCoefficientRestrict nu K omega = { toFun := fun (x : ↑K) => Algsuperdiff.Section5.Field.streamCoefficient nu omega ↑x, continuous_toFun := ⋯ }

@[simp]

theorem Algsuperdiff.Section5.Measurability.streamCoefficientRestrict_apply {d : ℕ} {gamma : ℝ} (nu : ℝ) (K : Set (HCPolySupport.Vec d)) (omega : Field.FullSample d gamma) (x : ↑K) : (streamCoefficientRestrict nu K omega) x = Field.streamCoefficient nu omega ↑x

theorem Algsuperdiff.Section5.Measurability.measurable_streamCoefficientRestrict {d : ℕ} {gamma : ℝ} (nu : ℝ) (K : Set (HCPolySupport.Vec d)) [CompactSpace ↑K] : Measurable (streamCoefficientRestrict nu K)

The full stream coefficient, restricted to any compact set, is a Borel measurable continuous matrix field.