Coarse-graining support: Support.Sobolev.H1.OriginCubeSymmetry

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

noncomputable def HCPolySupport.signFlipVecContinuousLinearEquiv {d : ℕ} (i : Fin d) : Vec d ≃L[ℝ] Vec d

Coordinate sign-flip on Vec d as a continuous linear equivalence.

Equations

• HCPolySupport.signFlipVecContinuousLinearEquiv i = ContinuousLinearEquiv.piCongrRight fun (j : Fin d) => if h : j = i then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ

noncomputable def HCPolySupport.swapVecContinuousLinearEquiv {d : ℕ} (i j : Fin d) : Vec d ≃L[ℝ] Vec d

Coordinate swap on Vec d as a continuous linear equivalence.

Equations

• HCPolySupport.swapVecContinuousLinearEquiv i j = ContinuousLinearEquiv.piCongrLeft ℝ (fun (x : Fin d) => ℝ) (Equiv.swap i j)

@[simp]

theorem HCPolySupport.signFlipVecContinuousLinearEquiv_apply {d : ℕ} (i : Fin d) (x : Vec d) : (signFlipVecContinuousLinearEquiv i) x = matVecMul (signFlipMatrix i) x

@[simp]

theorem HCPolySupport.signFlipVecContinuousLinearEquiv_symm_apply {d : ℕ} (i : Fin d) (x : Vec d) : (signFlipVecContinuousLinearEquiv i).symm x = matVecMul (signFlipMatrix i) x

@[simp]

theorem HCPolySupport.swapVecContinuousLinearEquiv_apply {d : ℕ} (i j : Fin d) (x : Vec d) : (swapVecContinuousLinearEquiv i j) x = matVecMul (Matrix.swap ℝ i j) x

@[simp]

theorem HCPolySupport.swapVecContinuousLinearEquiv_symm_apply {d : ℕ} (i j : Fin d) (x : Vec d) : (swapVecContinuousLinearEquiv i j).symm x = matVecMul (Matrix.swap ℝ i j) x

theorem HCPolySupport.signFlipVecContinuousLinearEquiv_self_apply {d : ℕ} (i : Fin d) (x : Vec d) : (signFlipVecContinuousLinearEquiv i) ((signFlipVecContinuousLinearEquiv i) x) = x

theorem HCPolySupport.swapVecContinuousLinearEquiv_self_apply {d : ℕ} (i j : Fin d) (x : Vec d) : (swapVecContinuousLinearEquiv i j) ((swapVecContinuousLinearEquiv i j) x) = x

theorem HCPolySupport.signFlipVecContinuousLinearEquiv_basisVec {d : ℕ} (i k : Fin d) : (signFlipVecContinuousLinearEquiv i) (basisVec k) = (if k = i then -1 else 1) • basisVec k

theorem HCPolySupport.swapVecContinuousLinearEquiv_basisVec {d : ℕ} (i j k : Fin d) : (swapVecContinuousLinearEquiv i j) (basisVec k) = basisVec ((Equiv.swap i j) k)

theorem HCPolySupport.measurePreserving_signFlipVecContinuousLinearEquiv_restrict_openCubeSet_originCube {d : ℕ} (i : Fin d) (n : ℤ) : MeasureTheory.MeasurePreserving (⇑(signFlipVecContinuousLinearEquiv i)) (MeasureTheory.volume.restrict (openCubeSet (originCube d n))) (MeasureTheory.volume.restrict (openCubeSet (originCube d n)))

theorem HCPolySupport.measurePreserving_swapVecContinuousLinearEquiv_restrict_openCubeSet_originCube {d : ℕ} (i j : Fin d) (n : ℤ) : MeasureTheory.MeasurePreserving (⇑(swapVecContinuousLinearEquiv i j)) (MeasureTheory.volume.restrict (openCubeSet (originCube d n))) (MeasureTheory.volume.restrict (openCubeSet (originCube d n)))

theorem HCPolySupport.setIntegral_comp_signFlipVecContinuousLinearEquiv_openCubeSet_originCube {d : ℕ} (i : Fin d) (n : ℤ) (f : Vec d → ℝ) : ∫ (x : Vec d) in openCubeSet (originCube d n), f ((signFlipVecContinuousLinearEquiv i) x) = ∫ (x : Vec d) in openCubeSet (originCube d n), f x

theorem HCPolySupport.setIntegral_comp_swapVecContinuousLinearEquiv_openCubeSet_originCube {d : ℕ} (i j : Fin d) (n : ℤ) (f : Vec d → ℝ) : ∫ (x : Vec d) in openCubeSet (originCube d n), f ((swapVecContinuousLinearEquiv i j) x) = ∫ (x : Vec d) in openCubeSet (originCube d n), f x

theorem HCPolySupport.fderiv_comp_signFlipVecContinuousLinearEquiv_apply_basisVec {d : ℕ} (i k : Fin d) {φ : Vec d → ℝ} {x : Vec d} (hφ : DifferentiableAt ℝ φ ((signFlipVecContinuousLinearEquiv i) x)) : (fderiv ℝ (fun (y : Vec d) => φ ((signFlipVecContinuousLinearEquiv i) y)) x) (basisVec k) = (if k = i then -1 else 1) * (fderiv ℝ φ ((signFlipVecContinuousLinearEquiv i) x)) (basisVec k)

theorem HCPolySupport.fderiv_comp_swapVecContinuousLinearEquiv_apply_basisVec {d : ℕ} (i j k : Fin d) {φ : Vec d → ℝ} {x : Vec d} (hφ : DifferentiableAt ℝ φ ((swapVecContinuousLinearEquiv i j) x)) : (fderiv ℝ (fun (y : Vec d) => φ ((swapVecContinuousLinearEquiv i j) y)) x) (basisVec ((Equiv.swap i j) k)) = (fderiv ℝ φ ((swapVecContinuousLinearEquiv i j) x)) (basisVec k)

theorem HCPolySupport.tsupport_comp_signFlip_subset_openCubeSet_originCube {d : ℕ} {f : Vec d → ℝ} (i : Fin d) (n : ℤ) (hsub : tsupport f ⊆ openCubeSet (originCube d n)) : (tsupport fun (x : Vec d) => f ((signFlipVecContinuousLinearEquiv i) x)) ⊆ openCubeSet (originCube d n)

theorem HCPolySupport.tsupport_comp_swap_subset_openCubeSet_originCube {d : ℕ} {f : Vec d → ℝ} (i j : Fin d) (n : ℤ) (hsub : tsupport f ⊆ openCubeSet (originCube d n)) : (tsupport fun (x : Vec d) => f ((swapVecContinuousLinearEquiv i j) x)) ⊆ openCubeSet (originCube d n)