LocalizationFluctuationJointCoeff

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

Joint (omega, x) measurability of the cutoff's doubled energy density

ABK26, l.approximate.recurrence.formula, Step 2, read at the recurrence pair (n, n+h).

The obligation this module discharges

LocalizationFluctuationMuMeasCore.stronglyMeasurable_doubledMuValue_of_jointly reduces sample-measurability of a doubled energy value to joint (omega, x) strong measurability of the integrand

  (omega, x) |->  blockEnergyDensityAt (a omega) (Z x) x .

At the Step-2 carriers the coefficient is meshCellCoeff M m R omega = (coefficientCutoffTriadicCoeffFamily M m omega).coeffOn R, so the sample enters the coefficient leg. This module supplies that leg, for an arbitrary (sample-independent) block field Z. The companion module LocalizationFluctuationJointField then removes the sample-independence of Z.

Method

Three proved facts about the genuine cutoff do all the work.

1. Caratheodory. Cutoff.continuous_cutoff_entry (continuity in the point) and Cutoff.measurable_cutoff_apply_entry (measurability in the sample) give joint measurability of every entry of k_m by measurable_uncurry_of_continuous_of_measurable. The corresponding uncurried statement inside Cutoff.Limit is private, so it is reproved here from the two public halves; no new mathematical content is introduced.

2. The symmetric part is deterministic. Cutoff.symmPart_coefficientCutoff says symm(a_m(omega, x)) = nu I identically. Hence the matrix inverse (symm a)^{-1} occurring in Book.Ch02.blockMatrixField is a constant matrix: no measurability of matrix inversion is needed anywhere below.

3. The skew part is the cutoff. skewPart_coefficientCutoff (proved here from Cutoff.cutoff_skew) identifies skew(a_m(omega, x)) = k_m(omega, x), whose entries are jointly measurable by 1.

Every entry of blockMatrixField is therefore a polynomial expression in jointly measurable entries and constants, and the doubled energy density is a finite sum of products of those entries with the components of Z.

Main results

• measurable_uncurry_cutoff_entry --- the joint measurability of the cutoff entries in the sample and the point.
• skewPart_coefficientCutoff, symmPart_meshCellCoeff --- the two pointwise identities that make the block matrix field polynomial.
• measurable_uncurry_blockMatrixField_meshCellCoeff_{upperLeft, upperRight, lowerLeft, lowerRight} --- the four entry families.
• measurable_uncurry_blockEnergyDensityAt_meshCellCoeff --- the joint measurability the reduction asks for, at a fixed block field.
• measurable_doubledMuValue_meshCellCoeff --- its consequence: at a fixed doubled field with measurable components, the doubled energy value is a measurable function of the sample.

Binders

Beyond the typing binders, only measurability of the two components of the fixed field. No integrability, no ellipticity, no smallness and no proposition about the corrector or the sample law occurs. Nothing here estimates anything.

Scope

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

References

• ABK26, l.approximate.recurrence.formula, Step 2, e.variational.mu.U.P.

The two pointwise identities of the genuine cutoff

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.skewPart_coefficientCutoff {d : ℕ} (nu : ℝ) (m : ℤ) (omega : Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) : HCPolySupport.skewPart ((Cutoff.coefficientCutoff nu m omega).toFun x) = (Cutoff.cutoff m omega).toFun x

The skew part of the coefficient cutoff is the cutoff itself. The representative is a_m = nu I + k_m with k_m skew, so the symmetric part is nu I (proved as Cutoff.symmPart_coefficientCutoff) and the skew part is k_m. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.symmPart_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) : HCPolySupport.symmPart ((meshCellCoeff M m R omega).toCoeffField x) = M.nu • 1

The symmetric part of the cell coefficient is the deterministic nu I.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.skewPart_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) (x : HCPolySupport.Vec d) : HCPolySupport.skewPart ((meshCellCoeff M m R omega).toCoeffField x) = (Cutoff.cutoff m omega).toFun x

The skew part of the cell coefficient is the cutoff.

Joint measurability of the cutoff entries

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_cutoff_entry {d : ℕ} (m : ℤ) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => (Cutoff.cutoff m p.1).toFun p.2 i j

Joint (omega, x) measurability of the genuine cutoff's entries. Caratheodory: continuous in the point, measurable in the sample. The corresponding statement inside Cutoff.Limit is private; this is the public form, reproved from the two public halves.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_matMul_entry {d : ℕ} {alpha : Type u_1} [MeasurableSpace alpha] {A B : alpha → HCPolySupport.Mat d} (hA : ∀ (i j : Fin d), Measurable fun (w : alpha) => A w i j) (hB : ∀ (i j : Fin d), Measurable fun (w : alpha) => B w i j) (i j : Fin d) : Measurable fun (w : alpha) => (A w * B w) i j

Entrywise measurability of a product of two entrywise-measurable matrix families. Elementary.

Joint measurability of the doubled block matrix field

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_skewPart_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => HCPolySupport.skewPart ((meshCellCoeff M m R p.1).toCoeffField p.2) i j

The skew leg of the cell coefficient, jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_matTranspose_skewPart_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => HCPolySupport.matTranspose (HCPolySupport.skewPart ((meshCellCoeff M m R p.1).toCoeffField p.2)) i j

The transposed skew leg, jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_skewT_mul_invSymm_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => (HCPolySupport.matTranspose (HCPolySupport.skewPart ((meshCellCoeff M m R p.1).toCoeffField p.2)) * (M.nu • 1)⁻¹) i j

The product k^t (nu I)^{-1}, entrywise jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_invSymm_mul_skew_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => ((M.nu • 1)⁻¹ * HCPolySupport.skewPart ((meshCellCoeff M m R p.1).toCoeffField p.2)) i j

The product (nu I)^{-1} k, entrywise jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_blockMatrixField_meshCellCoeff_upperLeft {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => (HCPolySupport.Book.Ch02.blockMatrixField (meshCellCoeff M m R p.1) p.2).upperLeft i j

The (1,1) block of bfA_m is jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_blockMatrixField_meshCellCoeff_upperRight {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => (HCPolySupport.Book.Ch02.blockMatrixField (meshCellCoeff M m R p.1) p.2).upperRight i j

The (1,2) block of bfA_m is jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_blockMatrixField_meshCellCoeff_lowerLeft {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => (HCPolySupport.Book.Ch02.blockMatrixField (meshCellCoeff M m R p.1) p.2).lowerLeft i j

The (2,1) block of bfA_m is jointly measurable.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_blockMatrixField_meshCellCoeff_lowerRight {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (i j : Fin d) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => (HCPolySupport.Book.Ch02.blockMatrixField (meshCellCoeff M m R p.1) p.2).lowerRight i j

The (2,2) block of bfA_m is deterministic, hence jointly measurable.

The joint measurability of the doubled energy density

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_uncurry_blockEnergyDensityAt_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) {Z : HCPolySupport.Vec d → HCPolySupport.BlockVec d} (hZ1 : ∀ (i : Fin d), Measurable fun (x : HCPolySupport.Vec d) => (Z x).1 i) (hZ2 : ∀ (i : Fin d), Measurable fun (x : HCPolySupport.Vec d) => (Z x).2 i) : Measurable fun (p : Cutoff.CutoffSample d × HCPolySupport.Vec d) => HCPolySupport.Book.Ch02.blockEnergyDensityAt (meshCellCoeff M m R p.1) (Z p.2) p.2

The doubled energy density of the cutoff, at a fixed block field, is jointly measurable in (omega, x).

This is the hypothesis hjoint of LocalizationFluctuationMuMeasCore.stronglyMeasurable_doubledMuValue_of_jointly whenever the competitor field does not depend on the sample.

only on measurability of the two components of Z.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.measurable_doubledMuValue_meshCellCoeff {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (W : HCPolySupport.Book.Ch02.DoubledField d) (hpot : Measurable W.potential) (hflux : Measurable W.flux) : Measurable fun (omega : Cutoff.CutoffSample d) => HCPolySupport.Book.Ch02.doubledMuValue (HCPolySupport.Book.Ch02.cubeDomain R) (meshCellCoeff M m R omega) W

The fixed-competitor sample measurability of the doubled energy value.

For a doubled field with measurable components the energy value on the cell is a measurable function of the sample. This is the shape the field-slope countable-infimum reduction of LocalizationFluctuationMuMeasCore consumes once the competitor has been made sample-independent.

only on measurability of the two components of W.