NuIdentification

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

The ν-identification of the coefficient energy

Throughout §4.3 the manuscript writes the local energy of a solution in three interchangeable ways:

  ⨍_V ∇u · a_L ∇u        (the coarse-graining lemmas)
  ⨍_V ∇u · symm(a) ∇u    (CoarseGraining's localizedCoeffEnergyValue)
  ν ⨍_V |∇u|²            (the manuscript's own "ν^{1/2}‖∇u‖")

The third form is ABK26; the ν^{1/2}‖∇u‖ it abbreviates is that of ABK26.

The three agree exactly, and the reason is the antisymmetric structure of the layer law: a_L = ν Id + k_L with k_L skew, so symm(a_L) = ν Id, and the skew part contributes nothing to a quadratic form. Subtracting the constant skew matrix (k_L − k_{n+2})_{z+□_{n+2}} does not disturb this: symm(ã_{L,n+2}) is still exactly ν Id.

This module closes it.

What is proved is an, and it is unconditional

That is weaker than the truth and the caps chain is not needed: the identity symm(ã_{L,k}) = ν Id holds for every sample and every point, so

  localizedCoeffEnergyValue V ã_{L,k} u = ν · ⨍_V |∇u|²

is an equality valid pointwise in ω, with no good event, no ellipticity ratio cap and no probabilistic input whatsoever. Both inequalities follow, and the ν^{1/2} form is obtained by taking square roots.

Main results

• vecDot_matVecMul_symmPart_self — the symmetric part is invisible on the diagonal: v · symm(A) v = v · A v for every matrix.
• localizedCoeffEnergyValue_eq_mul_of_symmPart_eq — the general identification for any coefficient object whose symmetric part is a constant multiple of the identity.
• sqrt_localizedCoeffEnergyValue_fluxCorrectedCoeffFamily — the printed ν^{1/2}‖∇u‖_{L²(V)} reading.

References

• ABK26, (⨍ ν|∇u|² as the energy base).
• CoarseGraining, Homogenization/Book/Ch03/Definitions.lean (localizedCoeffEnergyValue), Homogenization/Ambient/Basic.lean (symmPart, skewPart, matTranspose_skewPart).

1. The symmetric part is invisible on the diagonal

2. The general identification

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedCoeffEnergyValue_eq_mul_of_symmPart_eq {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (V : Set (HCPolySupport.Vec d)) (a : HCPolySupport.Book.Ch02.CoeffOn U) (u : HCPolySupport.H1Function U.carrier) (nu : ℝ) (hsymm : ∀ (x : HCPolySupport.Vec d), HCPolySupport.symmPart (a.toCoeffField x) = nu • 1) : HCPolySupport.Book.Ch03.localizedCoeffEnergyValue V a u = nu * HCPolySupport.Book.Ch03.normalizedSetAverage V fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad x)

The ν-identification, general form. If the symmetric part of the coefficient representative is ν Id at every point, the localized coefficient energy is exactly ν times the normalized gradient L² square.

3. The identification at the flux-corrected family

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedCoeffEnergyValue_fluxCorrectedCoeffFamily_eq {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (Q R : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) (V : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain R).carrier) : HCPolySupport.Book.Ch03.localizedCoeffEnergyValue V ((Support.fluxCorrectedCoeffFamily M L k Q omega).coeffOn R) u = M.nu * HCPolySupport.Book.Ch03.normalizedSetAverage V fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad x)

The ν-identification at the shifted field.

No good event, no ellipticity cap, no hypothesis on the sample.

4. The printed ν^{1/2}‖∇u‖ form

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_localizedCoeffEnergyValue_fluxCorrectedCoeffFamily {d : ℕ} (M : Section3.ABKModel d) (L k : ℤ) (Q R : HCPolySupport.TriadicCube d) (omega : Section3.Cutoff.CutoffSample d) (V : Set (HCPolySupport.Vec d)) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain R).carrier) : √(HCPolySupport.Book.Ch03.localizedCoeffEnergyValue V ((Support.fluxCorrectedCoeffFamily M L k Q omega).coeffOn R) u) = √M.nu * √(HCPolySupport.Book.Ch03.normalizedSetAverage V fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (u.grad x))

The manuscript's ν^{1/2}‖∇u‖_{L²(V)}. The square root of the localized coefficient energy of ã_{L,k} factors exactly as ν^{1/2} times the normalized gradient L² norm — the form in which write the energy.