PrincipalResponsePz

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

Provider: the localized loads P_z = (p_z; q_z) and F_z

Source displays in ABK26:

• e.Pz.def (label; display):

  P_z = (p_z; q_z)
    := bfAhom_{m-h}^{-1/2} ( e' + (grad w_{D,e}^{(K)})_{z+cu_n};
  e  + (grad w_{N,e'}^{(K)}
                                    + shom_{m-h}^{-1} h e')_{z+cu_n} ) ,
  

• e.Fz.def (label; display):

  F_z := bfAhom_{m-h}^{-1/2}
           ( grad w_{D,e}^{(K)} - (grad w_{D,e}^{(K)})_{z+cu_n};
  grad w_{N,e'}^{(K)} + shom_{m-h}^{-1} h e'
               - (grad w_{N,e'}^{(K)} + shom_{m-h}^{-1} h e')_{z+cu_n} ) ,
  

  where h = k_m - k_{m-h} is the fresh shell and (.)_{z+cu_n} is the average over the localization cube.

F_z is a field on R^d; P_z is the constant vector obtained from the same two fields by averaging them first, so that the affine background is P_z + F_z. That identity is principalPz_add_principalFz below.

Carriers, and what is and is not a hypothesis

• The normalization scale and the forcing scale are the same scale m - h in the source, so a single sigma : PositiveScalar supplies both here; a caller cannot accidentally mismatch them.
• The fresh shell is Cutoff.finiteShellIncrement omega lowScale highScale, entering through the repository's already-proved Provider.Diffusivity.Corrector.streamForcing, i.e. the forcing of e.def.w. In l.approximate.recurrence.formula the two scales are lowScale = m - h and highScale = m.
• The localization cube of the source is z + cu_n with n = m - h - 16 ceil |log_3 gamma| (e.recurrence.params, display, label). It enters below only as a free TriadicCube argument R. No literal buffer constant occurs in this module.
• The two correctors enter as the arguments wD and wN of e.def.w's carriers, exactly as in the already-proved FreshShellL8, FreshShellCZ, FreshShellExistence and FreshShellUniqueness, which quantify over solutions rather than selecting one. Consequently principalPz and principalFz are functions of the correctors: they are the manuscript's P_z and F_z exactly when wD and wN are solutions of e.def.w, whose existence and gradient-uniqueness are those two modules. No solution property is smuggled in as a hypothesis, and only the two gradient fields matter: Closure.JunctionDischargePrincipalSwitch.principalPz_congr_ae records that almost everywhere equal corrector gradients give the same load.

Main results

• neumannFluxField, principalPz, principalFz
• principalPz_fst, principalPz_snd (the components p_z and q_z)
• principalPz_add_principalFz

The flux leg field

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.neumannFluxField {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.Vec d → HCPolySupport.Vec d

The flux leg field of e.Pz.def and e.Fz.def: grad w_N + shom^{-1} (k_high - k_low) e'.

The additive term is the repository's streamForcing, i.e. the forcing of the Neumann problem e.def.w (label, Neumann leg), at the reciprocal of the same positive scalar that normalizes the load.

Equations

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

P_z

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalPz {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.BlockVec d

e.Pz.def. The localized principal load

P_z = bfAhom^{-1/2} ( e' + (grad w_D)_R; e + (grad w_N + shom^{-1} h e')_R ) ,

with R the localization cube. Its two components (P_z).1 and (P_z).2 are the manuscript's p_z and q_z; their closed forms are principalPz_fst and principalPz_snd.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalPz_fst {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : (principalPz sigma omega lowScale highScale e e' R wD wN).1 = Observable.inverseSqrtLoad sigma (e' + HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => wD.grad x)

p_z, the potential component of e.Pz.def.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalPz_snd {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : (principalPz sigma omega lowScale highScale e e' R wD wN).2 = Observable.sqrtLoad sigma (e + HCPolySupport.cubeAverageVec R (neumannFluxField sigma omega lowScale highScale e' wN))

q_z, the flux component of e.Pz.def.

F_z

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalFz {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.Vec d → HCPolySupport.BlockVec d

e.Fz.def. The mean-zero fluctuation field

F_z(x) = bfAhom^{-1/2} ( grad w_D(x) - (grad w_D)_R;
  (grad w_N + shom^{-1} h e')(x)
                           - (grad w_N + shom^{-1} h e')_R ) .

Unlike P_z it does not involve e, exactly as printed.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalFz_fst {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (x : HCPolySupport.Vec d) : (principalFz sigma omega lowScale highScale e' R wD wN x).1 = Observable.inverseSqrtLoad sigma (wD.grad x - HCPolySupport.cubeAverageVec R fun (y : HCPolySupport.Vec d) => wD.grad y)

The potential component of F_z.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalFz_snd {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (x : HCPolySupport.Vec d) : (principalFz sigma omega lowScale highScale e' R wD wN x).2 = Observable.sqrtLoad sigma (neumannFluxField sigma omega lowScale highScale e' wN x - HCPolySupport.cubeAverageVec R (neumannFluxField sigma omega lowScale highScale e' wN))

The flux component of F_z.

The affine background

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalPz_add_principalFz {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (x : HCPolySupport.Vec d) : principalPz sigma omega lowScale highScale e e' R wD wN + principalFz sigma omega lowScale highScale e' R wD wN x = principalLoad sigma (e' + wD.grad x, e + neumannFluxField sigma omega lowScale highScale e' wN x)

. P_z + F_z is the normalized unaveraged slope pair, i.e. the affine background inside which the source's X_z is minimized. This is the identity behind the split X_z = S_z + tilde S_z recorded at tex