Coarse-graining support: Support.Geometry.Translation

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

def HCPolySupport.translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : Set (Vec d)

Translate a set in Vec d by the vector z.

Equations

• HCPolySupport.translateSet z U = {x : HCPolySupport.Vec d | ∃ y ∈ U, x = y + z}

theorem HCPolySupport.mem_translateSet_iff_sub_mem {d : ℕ} {z x : Vec d} {U : Set (Vec d)} : x ∈ translateSet z U ↔ x - z ∈ U

theorem HCPolySupport.preimage_subRight_eq_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : (fun (x : Vec d) => x - z) ⁻¹' U = translateSet z U

theorem HCPolySupport.preimage_addNeg_eq_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : (fun (x : Vec d) => x + -z) ⁻¹' U = translateSet z U

theorem HCPolySupport.preimage_addRight_translateSet_eq {d : ℕ} (z : Vec d) (U : Set (Vec d)) : (fun (x : Vec d) => x + z) ⁻¹' translateSet z U = U

theorem HCPolySupport.image_addRight_eq_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : (fun (x : Vec d) => x + z) '' U = translateSet z U

theorem HCPolySupport.translateSet_inter {d : ℕ} (z : Vec d) (U V : Set (Vec d)) : translateSet z (U ∩ V) = translateSet z U ∩ translateSet z V

@[simp]

theorem HCPolySupport.translateSet_zero {d : ℕ} (U : Set (Vec d)) : translateSet 0 U = U

theorem HCPolySupport.translateSet_translateSet {d : ℕ} (z w : Vec d) (U : Set (Vec d)) : translateSet w (translateSet z U) = translateSet (z + w) U

theorem HCPolySupport.measurePreserving_subRight_restrict_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => x - z) (MeasureTheory.volume.restrict (translateSet z U)) (MeasureTheory.volume.restrict U)

theorem HCPolySupport.measurePreserving_addRight_restrict_translateSet {d : ℕ} (z : Vec d) (U : Set (Vec d)) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => x + z) (MeasureTheory.volume.restrict U) (MeasureTheory.volume.restrict (translateSet z U))

theorem HCPolySupport.setIntegral_comp_subRight_translateSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : Vec d) (U : Set (Vec d)) (f : Vec d → E) : ∫ (x : Vec d) in translateSet z U, f (x - z) = ∫ (y : Vec d) in U, f y

theorem HCPolySupport.setIntegral_comp_addRight_translateSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : Vec d) (U : Set (Vec d)) (f : Vec d → E) : ∫ (y : Vec d) in U, f (y + z) = ∫ (x : Vec d) in translateSet z U, f x

theorem HCPolySupport.volume_translateSet_eq {d : ℕ} (z : Vec d) (U : Set (Vec d)) : MeasureTheory.volume (translateSet z U) = MeasureTheory.volume U