GammaTenEnvelopeInputGauge

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

The Besov tower of the gauged bfF_z is a constant multiple of the raw one

ABK26, Step 2 of l.approximate.recurrence.formula, e.Fz.def.

What this module does

Closure.GammaTenCloserAssembly.ClosureBesovEnvelopeInput is stated at the two legs of the gauged field bfA_0^{1/2} bfF_z, i.e. at

  x |->  ( blockGaugeUp sigma_0 ( (localizationFz shom_n omega n (n+h) e' R wD wN).eval x ) ).1
  x |->  ( blockGaugeUp sigma_0 ( (localizationFz shom_n omega n (n+h) e' R wD wN).eval x ) ).2 .

LocalizationFluctuationOrthogonality identifies the two legs of bfF_z as scaled cube fluctuations of the two raw fields --- the Dirichlet corrector gradient and the Neumann flux field. Since the gauge is a scalar, each gauged leg is a constant multiple of a cube fluctuation, and the finite-depth positive q = 2 Besov seminorm is

• absolutely homogeneous in a scalar multiple, and
• unchanged by subtracting a constant --- which is what cubeFluctuationVec R does --- by CoarseGraining's cubeBesovPositiveVectorPartialSeminormTwo_sub_const.

Consequently the entire Besov tower of each gauged leg is a fixed scalar times the tower of the corresponding raw field, and the oscillation input of Step 2 never has to be read at the gauged field at all: it suffices to control the oscillation of grad w_D and of neumannFluxField, which is exactly what LocalizationOscillationDisplay's free-buffer display does.

What is proved

• cubeLpNorm_const_smul_vec, cubeFluctuationVec_const_smul --- homogeneity of the two building blocks.
• cubeBesovPositiveVectorDepthAverage_const_smul, cubeBesovPositiveVectorPartialSeminormTwo_const_smul --- homogeneity of the depth average (degree 2) and of the seminorm (degree 1).
• cubeBesovPositiveVectorPartialSeminormTwo_cubeFluctuationVec --- the tower does not see the cube fluctuation.
• cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_potential and ..._flux --- the two identities: the tower of each gauged leg equals the scalar |sqrt sigma_0 . sqrt shom_n^{-1}|, resp. |sqrt sigma_0^{-1} . sqrt shom_n|, times the tower of the raw field.

Binders

Only the L^2 membership of the raw field on the descendants of the cell, the standing integrability that makes the subtracted cube average finite. No smallness gate, no moment, no measurability and no sample-space proposition occurs.

Scope

Internal Provider infrastructure for the Step-2 fluctuation estimate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, e.Fz.def, Step 2 of l.approximate.recurrence.formula.

Homogeneity of the tower

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeLpNorm_const_smul_vec {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p : ENNReal) (c : ℝ) (v : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.cubeLpNorm Q p fun (x : HCPolySupport.Vec d) => c • v x) = |c| * HCPolySupport.cubeLpNorm Q p v

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFluctuationVec_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.cubeFluctuationVec Q fun (x : HCPolySupport.Vec d) => c • u x) = fun (x : HCPolySupport.Vec d) => c • HCPolySupport.cubeFluctuationVec Q u x

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeBesovPositiveVectorDepthAverage_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : HCPolySupport.cubeBesovPositiveVectorDepthAverage Q (fun (x : HCPolySupport.Vec d) => c • u x) j = c ^ 2 * HCPolySupport.cubeBesovPositiveVectorDepthAverage Q u j

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeBesovPositiveVectorPartialSeminormTwo_const_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (c : ℝ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => c • u x) = |c| * HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeBesovPositiveVectorPartialSeminormTwo_cubeFluctuationVec {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hmem : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ HCPolySupport.descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (HCPolySupport.normalizedCubeMeasure R)) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N (HCPolySupport.cubeFluctuationVec Q u) = HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N u

The tower does not see the cube fluctuation.

on the L^2 membership of the field on the descendants of Q, the standing integrability that makes the subtracted cube average finite.

The two gauged legs

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_potential {d : ℕ} (sig0 : ℝ) (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Qc : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Qc)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Qc)) (s : ℝ) (N : ℕ) (hmem : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ HCPolySupport.descendantsAtDepth R j, MeasureTheory.MemLp wD.grad 2 (HCPolySupport.normalizedCubeMeasure S)) : (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp sig0 ((localizationFz sigma omega lowScale highScale e' R wD wN).eval x)).1) = |√sig0 * (√↑sigma)⁻¹| * HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R s N wD.grad

The potential leg of the gauged bfF_z, at the Besov tower. Its tower on R is the scalar |sqrt sigma_0 . (sqrt shom)^{-1}| times the tower of the raw Dirichlet corrector gradient.

on the L^2 membership hmem of the raw gradient.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeBesovPositiveVectorPartialSeminormTwo_gauged_localizationFz_flux {d : ℕ} (sig0 : ℝ) (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Qc : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Qc)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Qc)) (s : ℝ) (N : ℕ) (hmem : ∀ j ∈ Finset.range (N + 1), ∀ S ∈ HCPolySupport.descendantsAtDepth R j, MeasureTheory.MemLp (neumannFluxField sigma omega lowScale highScale e' wN) 2 (HCPolySupport.normalizedCubeMeasure S)) : (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp sig0 ((localizationFz sigma omega lowScale highScale e' R wD wN).eval x)).2) = |(√sig0)⁻¹ * √↑sigma| * HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R s N (neumannFluxField sigma omega lowScale highScale e' wN)

The flux leg of the gauged bfF_z, at the Besov tower. Its tower on R is the scalar |(sqrt sigma_0)^{-1} . sqrt shom| times the tower of the raw Neumann flux field.

on the L^2 membership hmem of the raw flux field.