HomStepFourIdentity

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

Theorem B, §4.5, Step 4: the energy identities

What Step 4 needs, and what is proved here

Step 4 has four ingredients. Two of them are identities and both are proved here, unconditionally:

1. The pointwise bilinear split

     ∇u·a∇u - ∇v·σ∇v  =  (a∇u - σ∇v)·∇v + a∇u·(∇u - ∇v),
   

   an identity of vecDot, true for every matrix A, scalar σ and pair of vectors.

2. The testing identity

     ⨍_{□_m} (∇u - ∇v)·a_L∇u  =  ⨍_{□_m} ∇v·σ_m(∇u - ∇v),
   

   testing_identity / volumeAverage_testing_identity. Both Dirichlet problems of the Dirichlet-pair display are tested against the SAME H¹₀(□_m) element u - v and the two weak identities are subtracted; the common forcing term -⨍ g·∇(u-v) cancels. The H¹₀ witness is produced from the two HasZeroTraceDifferenceOn fields at the shared datum h (exists_h10Function_grad_eq_sub) — nothing is subtracted through the operator, and no boundary datum is removed from either equation.

3. The two duality pairings — HomStepFourPairing.

4. The Schauder bound on ‖∇v‖_{W^{s,∞}(□_m)} — NOT provable from the paper; see HomStepFourEnergy's disclosure.

The ν-drop

The theorem's conclusion, the introduction's energy display, is stated at ⨍ ν|∇u|² while the proof works with ⨍ ∇u·a_L∇u. The two agree exactly because the symmetric part of a_L = ν Id + κ is ν Id: vecDot_matVecMul_self_of_symmPart_smul_one. The manuscript never states this passage (a gap in the source at Step 4 (the energy identity)); it is proved here as a pointwise identity, ν is never divided by anything, and no ellipticity is used.

1. vecDot algebra

theorem Algsuperdiff.Section4.Provider.Homogenization.vecDot_sub_left {d : ℕ} (x y z : HCPolySupport.Vec d) : HCPolySupport.vecDot (x - y) z = HCPolySupport.vecDot x z - HCPolySupport.vecDot y z

Bilinearity of vecDot on the left.

theorem Algsuperdiff.Section4.Provider.Homogenization.vecDot_sub_right {d : ℕ} (x y z : HCPolySupport.Vec d) : HCPolySupport.vecDot x (y - z) = HCPolySupport.vecDot x y - HCPolySupport.vecDot x z

Bilinearity of vecDot on the right.

theorem Algsuperdiff.Section4.Provider.Homogenization.matVecMul_smul_one {d : ℕ} (c : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.matVecMul (c • 1) x = c • x

(c • Id) x = c • x.

theorem Algsuperdiff.Section4.Provider.Homogenization.vecDot_matVecMul_self_of_symmPart_smul_one {d : ℕ} {A : HCPolySupport.Mat d} {nu : ℝ} (hA : HCPolySupport.symmPart A = nu • 1) (xi : HCPolySupport.Vec d) : HCPolySupport.vecDot xi (HCPolySupport.matVecMul A xi) = nu * HCPolySupport.vecNormSq xi

The ν-drop, pointwise. If the symmetric part of A is ν Id then ξ · A ξ = ν |ξ|² — the identity behind the manuscript's silent passage between ⨍ ∇u · a_L ∇u and the theorem's ⨍ ν |∇u|² (a correction to the printed statement).

3. The H¹₀ witness for u - v

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_h10Function_grad_eq_sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u v h : HCPolySupport.H1Function U} (hu : Support.HasZeroTraceDifferenceOn U u h) (hv : Support.HasZeroTraceDifferenceOn U v h) : ∃ (w : HCPolySupport.H10Function U), ∀ (x : HCPolySupport.Vec d), w.grad x = u.grad x - v.grad x

u - v ∈ H¹₀(□_m): two solutions of the two Dirichlet problems with the SAME boundary datum h differ by an H¹₀ element. Only the two HasZeroTraceDifferenceOn witnesses are used; the datum h cancels and is never pushed through either operator.

4. The testing identity

theorem Algsuperdiff.Section4.Provider.Homogenization.testing_identity {d : ℕ} {A B : HCPolySupport.CoeffField d} {U : Set (HCPolySupport.Vec d)} {u v : HCPolySupport.H1Function U} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {w : HCPolySupport.H10Function U} (hu : Support.IsDivFormWeakSolutionOn A U u g) (hv : Support.IsDivFormWeakSolutionOn B U v g) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (HCPolySupport.matVecMul (A x) (u.grad x)) (w.grad x) = ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (HCPolySupport.matVecMul (B x) (v.grad x)) (w.grad x)

Testing both equations with u - v and subtracting.

Both weak formulations are evaluated at the same test function w ∈ H¹₀(□_m); the two right-hand sides are the SAME functional -∫ g·∇w of the SAME forcing g, so they cancel on subtraction. Nothing is divided, nothing is subtracted through an operator, and the boundary datum never appears.

theorem Algsuperdiff.Section4.Provider.Homogenization.testing_identity_gradDiff {d : ℕ} {A : HCPolySupport.CoeffField d} {U : Set (HCPolySupport.Vec d)} {sigma : ℝ} {u v h : HCPolySupport.H1Function U} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : Support.IsDivFormWeakSolutionOn A U u g) (hv : Support.IsDivFormWeakSolutionOn (fun (x : HCPolySupport.Vec d) => sigma • 1) U v g) (hbu : Support.HasZeroTraceDifferenceOn U u h) (hbv : Support.HasZeroTraceDifferenceOn U v h) : ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (HCPolySupport.matVecMul (A x) (u.grad x)) (u.grad x - v.grad x) = sigma * ∫ (x : HCPolySupport.Vec d) in U, HCPolySupport.vecDot (v.grad x) (u.grad x - v.grad x)

The testing identity at the gradient difference, with the scalar comparator B = σ Id evaluated: ⨍_{□}(a∇u)·(∇u-∇v) = σ ⨍_{□} ∇v·(∇u-∇v).