Coarse-graining support: Support.Sobolev.Foundations.PoincareSegment

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

Convex-domain segment geometry

This file isolates the algebraic and convexity lemmas for the segment parametrization

y ↦ y + t • (x - y),

which is the geometric core of the direct bounded-open-convex-domain Poincare proof. The later analytic files should be able to import this one and work only with segment identities, convex-membership statements, and MapsTo packaging, without redoing the affine algebra each time.

noncomputable def HCPolySupport.segmentBlend {d : ℕ} (x : Vec d) (t : ℝ) (y : Vec d) : Vec d

The point on the segment from y to x with parameter t.

Equations

• HCPolySupport.segmentBlend x t y = (AffineMap.lineMap y x) t

@[simp]

theorem HCPolySupport.segmentBlend_eq_lineMap {d : ℕ} (x y : Vec d) (t : ℝ) : segmentBlend x t y = (AffineMap.lineMap y x) t

theorem HCPolySupport.segmentBlend_zero {d : ℕ} (x y : Vec d) : segmentBlend x 0 y = y

theorem HCPolySupport.segmentBlend_one {d : ℕ} (x y : Vec d) : segmentBlend x 1 y = x

theorem HCPolySupport.segmentBlend_self {d : ℕ} (x : Vec d) (t : ℝ) : segmentBlend x t x = x

theorem HCPolySupport.segmentBlend_eq_add_smul_sub {d : ℕ} (x y : Vec d) (t : ℝ) : segmentBlend x t y = y + t • (x - y)

theorem HCPolySupport.segmentBlend_eq_smul_add {d : ℕ} (x y : Vec d) (t : ℝ) : segmentBlend x t y = (1 - t) • y + t • x

theorem HCPolySupport.add_smul_sub_eq_segmentBlend {d : ℕ} (x y : Vec d) (t : ℝ) : x + t • (y - x) = segmentBlend y t x

theorem HCPolySupport.segmentBlend_sub_right {d : ℕ} (x y : Vec d) (t : ℝ) : segmentBlend x t y - y = t • (x - y)

theorem HCPolySupport.left_sub_segmentBlend {d : ℕ} (x y : Vec d) (t : ℝ) : x - segmentBlend x t y = (1 - t) • (x - y)

theorem HCPolySupport.norm_segmentBlend_sub_right {d : ℕ} (x y : Vec d) (t : ℝ) : ‖segmentBlend x t y - y‖ = |t| * ‖x - y‖

theorem HCPolySupport.norm_left_sub_segmentBlend {d : ℕ} (x y : Vec d) (t : ℝ) : ‖x - segmentBlend x t y‖ = |1 - t| * ‖x - y‖

theorem HCPolySupport.segmentBlend_mem {d : ℕ} {U : Set (Vec d)} (hU : Convex ℝ U) {x y : Vec d} (hx : x ∈ U) (hy : y ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : segmentBlend x t y ∈ U

theorem HCPolySupport.segmentBlend_mapsTo {d : ℕ} {U : Set (Vec d)} (hU : Convex ℝ U) {x : Vec d} (hx : x ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Set.MapsTo (segmentBlend x t) U U

theorem HCPolySupport.segmentBlend_mem_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x y : Vec d} (hx : x ∈ U) (hy : y ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : segmentBlend x t y ∈ U

theorem HCPolySupport.segmentBlend_mapsTo_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x : Vec d} (hx : x ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Set.MapsTo (segmentBlend x t) U U

theorem HCPolySupport.ray_mem_of_endpoint_mem_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x ω : Vec d} {s t : ℝ} (hx : x ∈ U) (hs : x + s • ω ∈ U) (hs0 : 0 ≤ s) (ht0 : 0 ≤ t) (hts : t ≤ s) : x + t • ω ∈ U