Translation

Support for the Armstrong–Vicol anomalous-diffusion formalization.

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

Translate a set in Vec d by the vector z.

Equations

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

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

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

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

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

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

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

@[simp]

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

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

theorem Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.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 Homogenization.volume_translateSet_eq {d : ℕ} (z : Vec d) (U : Set (Vec d)) : MeasureTheory.volume (translateSet z U) = MeasureTheory.volume U