Signed coordinate transformations preserve the kernel and commute with infimal smoothing.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lowerKernelPhi_signed_invariant {d : ℕ} {p r theta : ℝ} (hp : 2 < p) (hr : r ≠ 0) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x : Point d) : lowerKernelPhi r theta (Q x) = lowerKernelPhi r theta x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpLinearMap_injective {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) : Function.Injective ⇑(signedLpLinearMap Q Qdual hsym)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.signedLpLinearMap_surjective {d : ℕ} {p : ℝ} (hp : 2 < p) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) : Function.Surjective ⇑(signedLpLinearMap Q Qdual hsym)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.smoothingCost_signed_change {d : ℕ} {p r theta chi : ℝ} (hp : 2 < p) (hr : r ≠ 0) (kernel : SmoothingKernelData p d) (hphi : kernel.phi = lowerKernelPhi r theta) (ell : Point d → ℝ) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x v : Point d) : Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi (fun (z : Point d) => ell (Q z)) x v = Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi ell (Q x) (Q v)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.localSmoothingValue_signed_equivariant {d : ℕ} {p r theta chi : ℝ} (hp : 2 < p) (hr : r ≠ 0) (kernel : SmoothingKernelData p d) (hphi : kernel.phi = lowerKernelPhi r theta) (ell : Point d → ℝ) {Q Qdual : Point d → Point d} (hsym : SignedLpSymmetry p Q Qdual) (x : Point d) : localSmoothingValue kernel chi (fun (z : Point d) => ell (Q z)) x = localSmoothingValue kernel chi ell (Q x)

Exact change of variables in the literal infimum.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_phi_signed_invariant {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (Q Qdual : Point d → Point d) : SignedLpSymmetry p Q Qdual → ∀ (x : Point d), (repairKernel p d).phi (Q x) = (repairKernel p d).phi x

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_smooth_value_signed_equivariant {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (chi : ℝ) : 0 < chi → ∀ (ell : Point d → ℝ) (Q Qdual : Point d → Point d), O3.IsConvexObjective ell → IsOneLipschitz p ell → SignedLpSymmetry p Q Qdual → ∀ (x : O3.Vec d), ((repairKernel p d).smooth chi fun (z : Point d) => ell (Q z)).value x = ((repairKernel p d).smooth chi ell).value (Q x)