Coarse-graining support: Support.Sobolev.PotentialSolenoidalOriginCubeBridge

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

theorem HCPolySupport.isPotentialOn_cubeSet_originCube_of_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {f : Vec d → Vec d} (hf : IsPotentialOn (openCubeSet (originCube d n)) f) : IsPotentialOn (cubeSet (originCube d n)) f

theorem HCPolySupport.isPotentialOn_openCubeSet_originCube_of_cubeSet {d : ℕ} {n : ℤ} {f : Vec d → Vec d} (hf : IsPotentialOn (cubeSet (originCube d n)) f) : IsPotentialOn (openCubeSet (originCube d n)) f

theorem HCPolySupport.isPotentialOn_cubeSet_originCube_iff_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {f : Vec d → Vec d} : IsPotentialOn (cubeSet (originCube d n)) f ↔ IsPotentialOn (openCubeSet (originCube d n)) f

theorem HCPolySupport.isPotentialZeroTraceOn_cubeSet_originCube_of_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn (openCubeSet (originCube d n)) f) : IsPotentialZeroTraceOn (cubeSet (originCube d n)) f

theorem HCPolySupport.isPotentialZeroTraceOn_openCubeSet_originCube_of_cubeSet {d : ℕ} [NeZero d] {n : ℤ} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn (cubeSet (originCube d n)) f) : IsPotentialZeroTraceOn (openCubeSet (originCube d n)) f

theorem HCPolySupport.isPotentialZeroTraceOn_cubeSet_originCube_iff_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {f : Vec d → Vec d} : IsPotentialZeroTraceOn (cubeSet (originCube d n)) f ↔ IsPotentialZeroTraceOn (openCubeSet (originCube d n)) f

theorem HCPolySupport.isSolenoidalOn_cubeSet_originCube_of_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {g : Vec d → Vec d} (hg : IsSolenoidalOn (openCubeSet (originCube d n)) g) : IsSolenoidalOn (cubeSet (originCube d n)) g

theorem HCPolySupport.isSolenoidalOn_openCubeSet_originCube_of_cubeSet {d : ℕ} [NeZero d] {n : ℤ} {g : Vec d → Vec d} (hg : IsSolenoidalOn (cubeSet (originCube d n)) g) : IsSolenoidalOn (openCubeSet (originCube d n)) g

theorem HCPolySupport.isSolenoidalOn_cubeSet_originCube_iff_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {g : Vec d → Vec d} : IsSolenoidalOn (cubeSet (originCube d n)) g ↔ IsSolenoidalOn (openCubeSet (originCube d n)) g

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_cubeSet_originCube_of_openCubeSet {d : ℕ} {n : ℤ} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) g) : IsSolenoidalZeroNormalTraceOn (cubeSet (originCube d n)) g

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_openCubeSet_originCube_of_cubeSet {d : ℕ} [NeZero d] {n : ℤ} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn (cubeSet (originCube d n)) g) : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) g

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_cubeSet_originCube_iff_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {g : Vec d → Vec d} : IsSolenoidalZeroNormalTraceOn (cubeSet (originCube d n)) g ↔ IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) g

theorem HCPolySupport.IsPotentialZeroTraceOn.integral_eq_zero_openCubeSet_originCube {d : ℕ} {n : ℤ} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn (openCubeSet (originCube d n)) f) : (fun (i : Fin d) => ∫ (x : Vec d) in openCubeSet (originCube d n), f x i) = 0

theorem HCPolySupport.IsPotentialZeroTraceOn.integral_eq_zero_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn (cubeSet (originCube d n)) f) : (fun (i : Fin d) => ∫ (x : Vec d) in cubeSet (originCube d n), f x i) = 0

theorem HCPolySupport.IsSolenoidalZeroNormalTraceOn.integral_eq_zero_openCubeSet_originCube {d : ℕ} {n : ℤ} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn (openCubeSet (originCube d n)) g) : (fun (i : Fin d) => ∫ (x : Vec d) in openCubeSet (originCube d n), g x i) = 0

theorem HCPolySupport.IsSolenoidalZeroNormalTraceOn.integral_eq_zero_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn (cubeSet (originCube d n)) g) : (fun (i : Fin d) => ∫ (x : Vec d) in cubeSet (originCube d n), g x i) = 0