Basic algebra of planeCrossProduct, the transitivity of the order it induces on the closed first quadrant, and the two shapes of level set used when a planar region is fanned into triangles over a base point.

source

@[simp]

theorem MovingSofa.planeCrossProduct_self (p : Point) :

planeCrossProduct p p = 0

source

@[simp]

theorem MovingSofa.planeCrossProduct_zero_left (p : Point) :

planeCrossProduct 0 p = 0

source

@[simp]

theorem MovingSofa.planeCrossProduct_zero_right (p : Point) :

planeCrossProduct p 0 = 0

source

theorem MovingSofa.planeCrossProduct_swap (p q : Point) :

planeCrossProduct p q = -planeCrossProduct q p

The oriented determinant is antisymmetric.

source

theorem MovingSofa.planeCrossProduct_eq_inner (p q : Point) :

planeCrossProduct p q = inner ℝ q !₂[-p.ofLp 1, p.ofLp 0]

The oriented determinant is the inner product against the quarter turn of its first argument.

source

theorem MovingSofa.planeCrossProduct_nonneg_trans {u v w : Point} (hv : v ≠ 0) (hu0 : 0 ≤ u.ofLp 0) (hu1 : 0 ≤ u.ofLp 1) (hv0 : 0 ≤ v.ofLp 0) (hv1 : 0 ≤ v.ofLp 1) (hw0 : 0 ≤ w.ofLp 0) (hw1 : 0 ≤ w.ofLp 1) (huv : 0 ≤ planeCrossProduct u v) (hvw : 0 ≤ planeCrossProduct v w) :

0 ≤ planeCrossProduct u w

In the closed first quadrant the oriented determinant order is transitive: if v is nonzero and both u × v and v × w are nonnegative, then so is u × w.

source

theorem MovingSofa.convex_setOf_planeCrossProduct_fan (u v L : Point) :

Convex ℝ {x : Point | 0 ≤ planeCrossProduct u (x - L) ∧ 0 ≤ planeCrossProduct (x - L) v}

The closed angular sector between two rays through a base point is convex.

source

theorem MovingSofa.volume_setOf_planeCrossProduct_sub_eq_zero {w : Point} (hw : w ≠ 0) (L : Point) :

MeasureTheory.volume {x : Point | planeCrossProduct w (x - L) = 0} = 0

The line through a base point in a nonzero direction carries no planar area.

source

theorem MovingSofa.planeCrossProduct_eq_inner_frame (a b : Point) (t : ℝ) :

planeCrossProduct a b = inner ℝ a (normalVector ↑t) * inner ℝ b (tangentVector ↑t) - inner ℝ a (tangentVector ↑t) * inner ℝ b (normalVector ↑t)

The planar cross product is the frame determinant at every angle.

source

theorem MovingSofa.planeCrossProduct_tangentVector (p : Point) (t : Real.Angle) :

planeCrossProduct p (tangentVector t) = inner ℝ p (normalVector t)

The oriented determinant of a point against the frame tangent is its normal coordinate.

Integral #

source

structure MovingSofa.RightContinuousIntervalBV (a b : ℝ) :

Type

A right-continuous real BV function on its actual closed-interval domain.

toFun : ↑(Set.Icc a b) → ℝ
The real-valued function on the closed parameter interval.
boundedVariation : IsIntervalBoundedVariation a b self.toFun
right_continuous (t : ↑(Set.Icc a b)) : ContinuousWithinAt self.toFun (Set.Ici t) t

Instances For

source

theorem MovingSofa.RightContinuousIntervalBV.toFun_injective {a b : ℝ} :

Function.Injective toFun

A right-continuous interval-BV function is determined by its underlying function.

source

theorem MovingSofa.RightContinuousIntervalBV.exists_norm_bound {a b : ℝ} (hab : a ≤ b) (f : RightContinuousIntervalBV a b) :

∃ (C : ℝ), ∀ (t : ↑(Set.Icc a b)), ‖f.toFun t‖ ≤ C

A right-continuous interval-BV function on a nonempty interval is bounded, by its value at the left endpoint plus the total variation.

source

noncomputable def MovingSofa.intervalStieltjesMeasure {a b : ℝ} (f : RightContinuousIntervalBV a b) :

MeasureTheory.SignedMeasure ↑(Set.Icc a b)

The finite signed Stieltjes measure on the interval, with zero initial atom.

Equations

MovingSofa.intervalStieltjesMeasure f = BoundedVariationOn.vectorMeasure ⋯

Instances For

source

noncomputable def MovingSofa.intervalStieltjesIntegral {a b : ℝ} (f : RightContinuousIntervalBV a b) (g : ↑(Set.Icc a b) → ℝ) (X : Set ↑(Set.Icc a b)) :

ℝ

The Stieltjes integral, used for bounded measurable integrands and Borel subsets.

Equations

MovingSofa.intervalStieltjesIntegral f g X = ∫ᵛ (t : ↑(Set.Icc a b)) in X, g t ∂[ContinuousLinearMap.mul ℝ ℝ; MovingSofa.intervalStieltjesMeasure f]

Instances For

source

theorem MovingSofa.intervalStieltjesIntegral_univ {a b : ℝ} (f : RightContinuousIntervalBV a b) (g : ↑(Set.Icc a b) → ℝ) :

intervalStieltjesIntegral f g Set.univ = MeasureTheory.VectorMeasure.integral (intervalStieltjesMeasure f) g (ContinuousLinearMap.mul ℝ ℝ)

Over the whole parameter interval, the interval Stieltjes integral is the unrestricted vector-measure integral.

Analysis / Stieltjes / Absolute Continuity #

source

noncomputable def MovingSofa.stieltjesScalarExtension {a b : ℝ} (f : RightContinuousIntervalBV a b) (t : ℝ) :

ℝ

Extend an interval function to the real line by zero outside its domain.

Equations

MovingSofa.stieltjesScalarExtension f t = if h : t ∈ Set.Icc a b then f.toFun ⟨t, h⟩ else 0

Instances For

source

def MovingSofa.HasIntervalStieltjesDensity {a b : ℝ} (f : RightContinuousIntervalBV a b) (r : ℝ → ℝ) :

Prop

An integrable density represents the interval Stieltjes measure on measurable sets.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MovingSofa.intervalStieltjesMeasure_Ioc {a b : ℝ} (f : RightContinuousIntervalBV a b) (c d : ↑(Set.Icc a b)) (hcd : c ≤ d) :

(intervalStieltjesMeasure f) (Set.Ioc c d) = f.toFun d - f.toFun c

source

theorem MovingSofa.intervalStieltjes_absoluteContinuity (a b : ℝ) (hab : a ≤ b) (f : RightContinuousIntervalBV a b) :

(AbsolutelyContinuousOnInterval (stieltjesScalarExtension f) a b ↔ ∃ (r : ℝ → ℝ), HasIntervalStieltjesDensity f r) ∧ ∀ (r : ℝ → ℝ), HasIntervalStieltjesDensity f r → ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), HasDerivAt (stieltjesScalarExtension f) (r t) t

Analysis / Stieltjes / Calculus #

source

theorem MovingSofa.intervalStieltjes_integration_by_parts (a b : ℝ) (hab : a ≤ b) (f g : RightContinuousIntervalBV a b) :

∃ (left : ↑(Set.Icc a b) → ℝ), (∀ (t : ↑(Set.Icc a b)), a < ↑t → Filter.Tendsto f.toFun (nhdsWithin t (Set.Iio t)) (nhds (left t))) ∧ intervalStieltjesIntegral f g.toFun {t : ↑(Set.Icc a b) | a < ↑t} + intervalStieltjesIntegral g left {t : ↑(Set.Icc a b) | a < ↑t} = f.toFun ⟨b, ⋯⟩ * g.toFun ⟨b, ⋯⟩ - f.toFun ⟨a, ⋯⟩ * g.toFun ⟨a, ⋯⟩

source

theorem MovingSofa.intervalStieltjes_integration_by_parts_Ioo (a b : ℝ) (hab : a < b) (f g : RightContinuousIntervalBV a b) :

intervalStieltjesIntegral g (Function.leftLim f.toFun) {t : ↑(Set.Icc a b) | a < ↑t ∧ ↑t < b} + intervalStieltjesIntegral f g.toFun {t : ↑(Set.Icc a b) | a < ↑t ∧ ↑t < b} = Function.leftLim f.toFun ⟨b, ⋯⟩ * Function.leftLim g.toFun ⟨b, ⋯⟩ - f.toFun ⟨a, ⋯⟩ * g.toFun ⟨a, ⋯⟩

Stieltjes integration by parts on the open interval (a, b): no endpoint atom is included at b, and none is introduced at a. The left limit in the first integrand accounts for simultaneous jumps.

source

theorem MovingSofa.intervalStieltjes_product (a b : ℝ) (f g : RightContinuousIntervalBV a b) (hcont : Continuous f.toFun ∨ Continuous g.toFun) :

∃ (h : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), h.toFun t = f.toFun t * g.toFun t) ∧ ∀ (E : Set ↑(Set.Icc a b)), MeasurableSet E → (intervalStieltjesMeasure h) E = intervalStieltjesIntegral f g.toFun E + intervalStieltjesIntegral g f.toFun E

source

theorem MovingSofa.intervalStieltjesIntegral_product_of_bounded {a b : ℝ} (hab : a ≤ b) (f g h : RightContinuousIntervalBV a b) (hgc : Continuous g.toFun) (hh : ∀ (t : ↑(Set.Icc a b)), h.toFun t = f.toFun t * g.toFun t) (φ : ↑(Set.Icc a b) → ℝ) (hφ : Measurable φ) (C : ℝ) (hφb : ∀ (t : ↑(Set.Icc a b)), ‖φ t‖ ≤ C) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) :

intervalStieltjesIntegral h φ E = intervalStieltjesIntegral f (fun (t : ↑(Set.Icc a b)) => φ t * g.toFun t) E + intervalStieltjesIntegral g (fun (t : ↑(Set.Icc a b)) => φ t * f.toFun t) E

The integrated Stieltjes product rule: a bounded measurable weight distributes over the Lebesgue–Stieltjes measure of a product one factor of which is continuous.

Analysis / Stieltjes / Density Integration #

source

theorem MovingSofa.intervalStieltjesIntegral_eq_integral_mul_of_density {a b : ℝ} (F : RightContinuousIntervalBV a b) {r : ℝ → ℝ} (hr : HasIntervalStieltjesDensity F r) {q : ↑(Set.Icc a b) → ℝ} (hq : Continuous q) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) :

intervalStieltjesIntegral F q E = ∫ (t : { x : ℝ // x ∈ Set.Icc a b }) in E, q t * r ↑t ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

A continuous integrand against an interval Stieltjes measure with an ordinary density is the corresponding weighted Lebesgue integral on the interval subtype.

source

theorem MovingSofa.intervalStieltjesIntegral_eq_integral_mul_of_density_bv {a b : ℝ} (hab : a ≤ b) (F : RightContinuousIntervalBV a b) {r : ℝ → ℝ} (hr : HasIntervalStieltjesDensity F r) {q : ↑(Set.Icc a b) → ℝ} (hq : BoundedVariationOn q Set.univ) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) :

intervalStieltjesIntegral F q E = ∫ (t : { x : ℝ // x ∈ Set.Icc a b }) in E, q t * r ↑t ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

The density formula also applies to a bounded-variation integrand on a nonempty compact interval.

source

theorem MovingSofa.RightContinuousIntervalBV.integrableOn_Icc_of_eq {a b : ℝ} (f : RightContinuousIntervalBV a b) (q : ℝ → ℝ) (hq : ∀ (t : ↑(Set.Icc a b)), q ↑t = f.toFun t) :

MeasureTheory.IntegrableOn q (Set.Icc a b) MeasureTheory.volume

A real function agreeing with a BV representative is integrable on its interval.

Analysis / Stieltjes / Linearity #

source

theorem MovingSofa.intervalStieltjes_linear_combination (a b : ℝ) (f g : RightContinuousIntervalBV a b) (r s : ℝ) :

∃ (h : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), h.toFun t = r * f.toFun t + s * g.toFun t) ∧ intervalStieltjesMeasure h = r • intervalStieltjesMeasure f + s • intervalStieltjesMeasure g

Analysis / Stieltjes / Inner Product #

source

theorem MovingSofa.intervalStieltjes_inner_fin_two {a b : ℝ} (f g : Fin 2 → RightContinuousIntervalBV a b) (hg : ∀ (i : Fin 2), Continuous (g i).toFun) :

∃ (h : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), h.toFun t = ∑ i : Fin 2, (f i).toFun t * (g i).toFun t) ∧ ∀ (E : Set ↑(Set.Icc a b)), MeasurableSet E → (intervalStieltjesMeasure h) E = ∑ i : Fin 2, (intervalStieltjesIntegral (f i) (g i).toFun E + intervalStieltjesIntegral (g i) (f i).toFun E)

Componentwise product rule for the Euclidean pairing of two planar interval-BV functions, when the second function is continuous.

Analysis / Stieltjes / Smooth #

source

theorem MovingSofa.exists_intervalBV_of_hasDerivAt {a b : ℝ} (hab : a ≤ b) (φ φ' : ℝ → ℝ) (hderiv : ∀ (t : ℝ), HasDerivAt φ (φ' t) t) (hφ' : Continuous φ') :

∃ (F : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), F.toFun t = φ ↑t) ∧ HasIntervalStieltjesDensity F φ'

A continuously differentiable real function restricted to a compact interval, together with its Stieltjes density.

source

theorem MovingSofa.hasIntervalStieltjesDensity_of_hasDerivAt {a b : ℝ} (hab : a ≤ b) (F : RightContinuousIntervalBV a b) (φ φ' : ℝ → ℝ) (hF : ∀ (t : ↑(Set.Icc a b)), F.toFun t = φ ↑t) (hac : AbsolutelyContinuousOnInterval φ a b) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt φ (φ' t) t) (hint : MeasureTheory.IntegrableOn φ' (Set.Icc a b) MeasureTheory.volume) :

HasIntervalStieltjesDensity F φ'

A right-continuous interval bounded-variation function that agrees on its interval with an absolutely continuous function differentiable on the open interval has that derivative as its Stieltjes density. Unlike exists_intervalBV_of_hasDerivAt this identifies the density of a given bounded-variation function, and asks for differentiability only in the interior.

Analysis / Stieltjes / Frame #

source

theorem MovingSofa.exists_normalVector_coordinate_intervalBV {a b : ℝ} (hab : a ≤ b) (i : Fin 2) :

∃ (F : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), F.toFun t = (normalVector ↑↑t).ofLp i) ∧ HasIntervalStieltjesDensity F fun (t : ℝ) => (tangentVector ↑t).ofLp i

A coordinate of the rotating normal frame is a continuous interval-BV function whose Stieltjes density is the corresponding tangent coordinate.

source

theorem MovingSofa.exists_tangentVector_coordinate_intervalBV {a b : ℝ} (hab : a ≤ b) (i : Fin 2) :

∃ (F : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), F.toFun t = (tangentVector ↑↑t).ofLp i) ∧ HasIntervalStieltjesDensity F fun (t : ℝ) => -(normalVector ↑t).ofLp i

A coordinate of the rotating tangent frame is a continuous interval-BV function whose Stieltjes density is the negative normal coordinate.

Analysis / Stieltjes / Transport #

source

theorem MovingSofa.intervalStieltjesIntegral_comp_monotone_surjective {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (F : RightContinuousIntervalBV a b) (hFc : Continuous F.toFun) (g : ↑(Set.Icc a b) → ℝ) (hgc : Continuous g) (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)) (hφc : Continuous φ) (hφ : Monotone φ) (hφs : Function.Surjective φ) :

intervalStieltjesIntegral F g Set.univ = intervalStieltjesIntegral { toFun := F.toFun ∘ φ, boundedVariation := ⋯, right_continuous := ⋯ } (g ∘ φ) Set.univ

Continuous monotone surjective reparametrization preserves the Stieltjes integral.

source

theorem MovingSofa.intervalStieltjesIntegral_Ioc_eq_inclusion {a b : ℝ} (F : RightContinuousIntervalBV a b) (hFc : Continuous F.toFun) (g : ↑(Set.Icc a b) → ℝ) (hgc : Continuous g) (l u : ↑(Set.Icc a b)) (hlu : l ≤ u) :

let ι := fun (x : ↑(Set.Icc ↑l ↑u)) => ⟨↑x, ⋯⟩; have hfr := ⋯; intervalStieltjesIntegral F g (Set.Ioc l u) = intervalStieltjesIntegral { toFun := F.toFun ∘ ι, boundedVariation := hfr, right_continuous := ⋯ } (g ∘ ι) Set.univ

Restricting a continuous Stieltjes integral agrees with integration on the subinterval.

source

theorem MovingSofa.intervalStieltjesIntegral_eq_sum_Ioc {a b : ℝ} (F : RightContinuousIntervalBV a b) (hFc : Continuous F.toFun) (g : ↑(Set.Icc a b) → ℝ) (hgc : Continuous g) {n : ℕ} (cuts : Fin (n + 1) → ↑(Set.Icc a b)) (hcuts : Monotone cuts) (hzero : ↑(cuts 0) = a) (hlast : ↑(cuts (Fin.last n)) = b) :

intervalStieltjesIntegral F g Set.univ = ∑ i : Fin n, intervalStieltjesIntegral F g (Set.Ioc (cuts i.castSucc) (cuts i.succ))

A continuous Stieltjes integral splits over a finite monotone partition.

source

theorem MovingSofa.intervalStieltjesIntegral_comp_reverse {a b : ℝ} (hab : a ≤ b) (F : RightContinuousIntervalBV a b) (hFc : Continuous F.toFun) (g : ↑(Set.Icc a b) → ℝ) (hgc : Continuous g) :

let r := Set.Icc.reverse hab; have hfr := ⋯; intervalStieltjesIntegral { toFun := F.toFun ∘ r, boundedVariation := hfr, right_continuous := ⋯ } (g ∘ r) Set.univ = -intervalStieltjesIntegral F g Set.univ

Reversing both continuous integrand and BV integrator negates their Stieltjes integral.

Analysis / Stieltjes / Continuous #

source

theorem MovingSofa.RightContinuousIntervalBV.integrable_of_continuous {a b : ℝ} (F : RightContinuousIntervalBV a b) {g : ↑(Set.Icc a b) → ℝ} (hg : Continuous g) :

MeasureTheory.VectorMeasure.Integrable (intervalStieltjesMeasure F) g

A continuous function is integrable against a BV Stieltjes measure on a compact interval.

source

theorem MovingSofa.intervalStieltjesIntegral_univ_eq_Ioo_of_continuous {a b : ℝ} (hab : a ≤ b) (F : RightContinuousIntervalBV a b) (hF : Continuous F.toFun) (g : ↑(Set.Icc a b) → ℝ) (hg : Continuous g) :

intervalStieltjesIntegral F g Set.univ = intervalStieltjesIntegral F g (Set.Ioo ⟨a, ⋯⟩ ⟨b, ⋯⟩)

For a continuous driver and a continuous integrand, the closed-interval Stieltjes integral agrees with the open-interval one: neither endpoint carries an atom.

source

theorem MovingSofa.intervalStieltjes_integration_by_parts_of_continuous (a b : ℝ) (hab : a ≤ b) (F G : RightContinuousIntervalBV a b) (hF : Continuous F.toFun) (hG : Continuous G.toFun) :

intervalStieltjesIntegral F G.toFun Set.univ + intervalStieltjesIntegral G F.toFun Set.univ = F.toFun ⟨b, ⋯⟩ * G.toFun ⟨b, ⋯⟩ - F.toFun ⟨a, ⋯⟩ * G.toFun ⟨a, ⋯⟩

Integration by parts for continuous BV functions on the full compact interval.

Analysis / Stieltjes / Affine #

source

theorem MovingSofa.intervalStieltjesMeasure_univ_of_continuous {a b : ℝ} (hab : a ≤ b) (Q : RightContinuousIntervalBV a b) (hQ : Continuous Q.toFun) :

(intervalStieltjesMeasure Q) Set.univ = Q.toFun ⟨b, ⋯⟩ - Q.toFun ⟨a, ⋯⟩

A continuous BV driver carries total Stieltjes mass equal to its increment.

source

theorem MovingSofa.intervalStieltjesMeasure_affine {a b : ℝ} (Q F : RightContinuousIntervalBV a b) (hQ : Continuous Q.toFun) (u v : ℝ) (hF : ∀ (t : ↑(Set.Icc a b)), F.toFun t = u + v * Q.toFun t) :

intervalStieltjesMeasure F = v • intervalStieltjesMeasure Q

An affine function of a continuous BV driver has that driver's Stieltjes measure, scaled by the affine map's slope.

source

theorem MovingSofa.intervalStieltjesIntegral_add_const {a b : ℝ} (hab : a ≤ b) (F G : RightContinuousIntervalBV a b) (hF : Continuous F.toFun) (c : ℝ) (hFG : ∀ (t : ↑(Set.Icc a b)), G.toFun t = F.toFun t + c) (g : ↑(Set.Icc a b) → ℝ) (hg : Continuous g) (d : ℝ) :

intervalStieltjesIntegral G (fun (t : ↑(Set.Icc a b)) => g t + d) Set.univ = intervalStieltjesIntegral F g Set.univ + d * (F.toFun ⟨b, ⋯⟩ - F.toFun ⟨a, ⋯⟩)

Shifting a continuous BV driver and its integrand by constants shifts the interval Stieltjes integral over the whole parameter interval by the integrand's shift times the driver's increment; the driver's own shift has no effect.

source

theorem MovingSofa.intervalStieltjesIntegral_affine_driver_cross {a b : ℝ} (hab : a ≤ b) (Q F G : RightContinuousIntervalBV a b) (hQ : Continuous Q.toFun) (u v w z : ℝ) (hF : ∀ (t : ↑(Set.Icc a b)), F.toFun t = u + v * Q.toFun t) (hG : ∀ (t : ↑(Set.Icc a b)), G.toFun t = w + z * Q.toFun t) :

intervalStieltjesIntegral G F.toFun Set.univ - intervalStieltjesIntegral F G.toFun Set.univ = (u * z - w * v) * (Q.toFun ⟨b, ⋯⟩ - Q.toFun ⟨a, ⋯⟩)

The signed cross integral of two affine functions of one continuous BV driver.

source

theorem MovingSofa.intervalStieltjesIntegral_affine_cross (F G : RightContinuousIntervalBV 0 1) (a b c d : ℝ) (hF : ∀ (t : ↑(Set.Icc 0 1)), F.toFun t = a + b * ↑t) (hG : ∀ (t : ↑(Set.Icc 0 1)), G.toFun t = c + d * ↑t) :

intervalStieltjesIntegral G F.toFun Set.univ - intervalStieltjesIntegral F G.toFun Set.univ = a * d - c * b

Riemann-Stieltjes sums for continuous integrands #

Left-endpoint sums over finite monotone partitions converge to the interval Stieltjes integral of a continuous integrand against a continuous BV integrator, uniformly in the mesh of the partition.

source

theorem MovingSofa.intervalStieltjesIntegral_sub_le_of_abs_sub_le {a b : ℝ} (F : RightContinuousIntervalBV a b) {g h : ↑(Set.Icc a b) → ℝ} (hg : MeasureTheory.VectorMeasure.Integrable (intervalStieltjesMeasure F) g) (hh : MeasureTheory.VectorMeasure.Integrable (intervalStieltjesMeasure F) h) {ε : ℝ} (hε : 0 ≤ ε) (hbound : ∀ᵐ (t : ↑(Set.Icc a b)) ∂MeasureTheory.VectorMeasure.variation (intervalStieltjesMeasure F), |g t - h t| ≤ ε) :

|intervalStieltjesIntegral F g Set.univ - intervalStieltjesIntegral F h Set.univ| ≤ ε * (MeasureTheory.VectorMeasure.variation (intervalStieltjesMeasure F)).real Set.univ

Two Stieltjes integrals differ by at most the uniform distance of their integrands times the total variation of the integrator.

source

theorem MovingSofa.intervalStieltjesIntegral_sub_sum_le_of_oscillation {a b : ℝ} (F : RightContinuousIntervalBV a b) (hF : Continuous F.toFun) {g : ↑(Set.Icc a b) → ℝ} (hg : Continuous g) {n : ℕ} (cuts : Fin (n + 1) → ↑(Set.Icc a b)) (hcuts : Monotone cuts) (hzero : ↑(cuts 0) = a) (hlast : ↑(cuts (Fin.last n)) = b) {ε : ℝ} (hε : 0 ≤ ε) (hosc : ∀ (i : Fin n), ∀ t ∈ Set.Ioc (cuts i.castSucc) (cuts i.succ), |g t - g (cuts i.castSucc)| ≤ ε) :

|intervalStieltjesIntegral F g Set.univ - ∑ i : Fin n, g (cuts i.castSucc) * (F.toFun (cuts i.succ) - F.toFun (cuts i.castSucc))| ≤ ε * (MeasureTheory.VectorMeasure.variation (intervalStieltjesMeasure F)).real Set.univ

The error in a left-endpoint Stieltjes sum is controlled by the cell oscillation of the integrand times the total variation of the integrator.

source

theorem MovingSofa.exists_mesh_bound_intervalStieltjesIntegral_sub_sum {a b : ℝ} (F : RightContinuousIntervalBV a b) (hF : Continuous F.toFun) {g : ↑(Set.Icc a b) → ℝ} (hg : Continuous g) {ε : ℝ} (hε : 0 < ε) :

∃ δ > 0, ∀ {n : ℕ} (cuts : Fin (n + 1) → ↑(Set.Icc a b)), Monotone cuts → ↑(cuts 0) = a → ↑(cuts (Fin.last n)) = b → (∀ (i : Fin n), ↑(cuts i.succ) - ↑(cuts i.castSucc) < δ) → |intervalStieltjesIntegral F g Set.univ - ∑ i : Fin n, g (cuts i.castSucc) * (F.toFun (cuts i.succ) - F.toFun (cuts i.castSucc))| ≤ ε * (MeasureTheory.VectorMeasure.variation (intervalStieltjesMeasure F)).real Set.univ

Sufficiently fine partitions approximate a continuous Stieltjes integrand uniformly.

source

theorem MovingSofa.tendsto_stieltjesSum_of_mesh_tendsto_zero {a b : ℝ} (F : RightContinuousIntervalBV a b) (hF : Continuous F.toFun) {g : ↑(Set.Icc a b) → ℝ} (hg : Continuous g) (N : ℕ → ℕ) (cuts : (k : ℕ) → Fin (N k + 1) → ↑(Set.Icc a b)) (hcuts : ∀ (k : ℕ), Monotone (cuts k)) (hzero : ∀ (k : ℕ), ↑(cuts k 0) = a) (hlast : ∀ (k : ℕ), ↑(cuts k (Fin.last (N k))) = b) (hmesh : ∀ δ > 0, ∀ᶠ (k : ℕ) in Filter.atTop , ∀ (i : Fin (N k)), ↑(cuts k i.succ) - ↑(cuts k i.castSucc) < δ) :

Filter.Tendsto (fun (k : ℕ) => ∑ i : Fin (N k), g (cuts k i.castSucc) * (F.toFun (cuts k i.succ) - F.toFun (cuts k i.castSucc))) Filter.atTop (nhds (intervalStieltjesIntegral F g Set.univ))

Left-endpoint Stieltjes sums converge along any family of partitions whose mesh tends to zero.

Analysis / Stieltjes / Shift #

source

theorem MovingSofa.exists_intervalBV_shift_add {a b c : ℝ} (hab : a ≤ b) (f : RightContinuousIntervalBV (a + c) (b + c)) (hfc : Continuous f.toFun) :

∃ (g : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), g.toFun t = f.toFun ⟨↑t + c, ⋯⟩) ∧ ∀ (E : Set ↑(Set.Icc a b)), MeasurableSet E → (intervalStieltjesMeasure g) E = (intervalStieltjesMeasure f) ((fun (t : ↑(Set.Icc a b)) => ⟨↑t + c, ⋯⟩) '' E)

Translate a continuous interval-BV representative and its Stieltjes measure.

source

theorem MovingSofa.exists_intervalBV_shift_from_zero {b c : ℝ} (hb : 0 ≤ b) (f : RightContinuousIntervalBV (0 + c) (b + c)) (hfc : Continuous f.toFun) :

∃ (g : RightContinuousIntervalBV 0 b), (∀ (t : ↑(Set.Icc 0 b)), g.toFun t = f.toFun ⟨↑t + c, ⋯⟩) ∧ ∀ (E : Set ↑(Set.Icc 0 b)), MeasurableSet E → (intervalStieltjesMeasure g) E = (intervalStieltjesMeasure f) ((fun (t : ↑(Set.Icc 0 b)) => ⟨↑t + c, ⋯⟩) '' E)

Specialize interval translation to an interval starting at zero.

Analysis / Surface Measure / Basic #

source

@[instance_reducible]

noncomputable instance MovingSofa.angleMeasurableSpace :

MeasurableSpace Real.Angle

Equations

MovingSofa.angleMeasurableSpace = borel Real.Angle

source

instance MovingSofa.angleBorelSpace :

BorelSpace Real.Angle

source

def MovingSofa.IsExteriorNormal (K : ConvexBody Point) (p : Point) (a : Real.Angle) :

Prop

An exterior normal direction at a point of a convex body.

Equations

MovingSofa.IsExteriorNormal K p a = ∀ q ∈ ↑K, inner ℝ (q - p) (MovingSofa.normalVector a) ≤ 0

Instances For

source

def MovingSofa.regularBoundary (K : ConvexBody Point) :

Set Point

Boundary points with exactly one exterior unit normal.

Equations

MovingSofa.regularBoundary K = {p : MovingSofa.Point | p ∈ frontier ↑K ∧ ∃! a : Real.Angle , MovingSofa.IsExteriorNormal K p a}

Instances For

source

noncomputable def MovingSofa.exteriorNormalAngle (K : ConvexBody Point) (p : Point) :

Real.Angle

The unique exterior normal at regular points, extended by zero elsewhere.

Equations

MovingSofa.exteriorNormalAngle K p = if h : ∃! a : Real.Angle , MovingSofa.IsExteriorNormal K p a then ⋯.choose else 0

Instances For

source

def MovingSofa.IsSegmentPresentation (K : ConvexBody Point) (d : Point × Point × Real.Angle) :

Prop

A nontrivial segment presentation and a perpendicular angular direction.

Equations

MovingSofa.IsSegmentPresentation K d = (d.1 ≠ d.2.1 ∧ ↑K = segment ℝ d.1 d.2.1 ∧ inner ℝ (d.2.1 - d.1) (MovingSofa.normalVector d.2.2) = 0)

Instances For

source

noncomputable def MovingSofa.surfaceAreaMeasure (K : ConvexBody Point) :

MeasureTheory.Measure Real.Angle

Surface measure in angular coordinates, including point and segment bodies.

Equations

One or more equations did not get rendered due to their size.

Instances For

Analysis / Surface Measure / Exterior Normal #

source

theorem MovingSofa.exists_isExteriorNormal_of_mem_frontier (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) {p : Point} (hp : p ∈ frontier ↑K) :

∃ (a : Real.Angle), IsExteriorNormal K p a

Every frontier point of a convex body with nonempty interior admits an exterior unit normal.

Analysis / Surface Measure / Graph Definitions #

source

def MovingSofa.horizontalProjection (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) :

Set ℝ

Project the convex body horizontally after translating and changing orthonormal frame.

Equations

MovingSofa.horizontalProjection K o e = (fun (p : MovingSofa.Point) => (e (p - o)).ofLp 0) '' ↑K

Instances For

source

noncomputable def MovingSofa.horizontalBounds (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) :

ℝ × ℝ

The infimum and supremum of the body’s horizontal projection in the chosen frame.

Equations

MovingSofa.horizontalBounds K o e = (sInf (MovingSofa.horizontalProjection K o e), sSup (MovingSofa.horizontalProjection K o e))

Instances For

source

noncomputable def MovingSofa.upperGraphHeight (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) (x : ℝ) :

ℝ

The supremum of the body’s vertical section at a given horizontal coordinate.

Equations

MovingSofa.upperGraphHeight K o e x = sSup {y : ℝ | o + e.symm !₂[x, y] ∈ ↑K}

Instances For

source

noncomputable def MovingSofa.vectorNormalAngle (p : Point) :

Real.Angle

The argument of a planar vector, viewed as an angle modulo a full turn.

Equations

MovingSofa.vectorNormalAngle p = ↑{ re := p.ofLp 0, im := p.ofLp 1 }.arg

Instances For

source

theorem MovingSofa.normalVector_vectorNormalAngle {p : Point} (hp : p ≠ 0) :

normalVector (vectorNormalAngle p) = ‖p‖⁻¹ • p

The normal vector associated to a nonzero planar vector is its normalization.

source

noncomputable def MovingSofa.upperGraphSurfaceIntegrand (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) (ψ : Real.Angle → ℝ) (x : ℝ) :

ℝ

Weight the upper graph by its normal direction and arc-length Jacobian.

Equations

One or more equations did not get rendered due to their size.

Instances For

Analysis / Surface Measure / Regularity #

source

instance MovingSofa.angleCompactSpace :

CompactSpace Real.Angle

source

theorem MovingSofa.continuous_normalVector_angle :

Continuous normalVector

The unit normal depends continuously on its angle.

source

theorem MovingSofa.measurableSet_regularBoundary (K : ConvexBody Point) :

MeasurableSet (regularBoundary K)

Points with a unique exterior normal form a Borel set.

source

theorem MovingSofa.continuousOn_exteriorNormalAngle_regularBoundary (K : ConvexBody Point) :

ContinuousOn (exteriorNormalAngle K) (regularBoundary K)

The exterior normal varies continuously on the regular boundary.

source

theorem MovingSofa.aemeasurable_exteriorNormalAngle_restrict_regularBoundary (K : ConvexBody Point) (μ : MeasureTheory.Measure Point) :

AEMeasurable (exteriorNormalAngle K) (μ.restrict (regularBoundary K))

The exterior normal is measurable for any measure restricted to the regular boundary.

Analysis / Surface Measure / Segment #

source

theorem MovingSofa.normalVector_eq_or_eq_add_pi_of_orthogonal {v : Point} (hv : v ≠ 0) {s t : Real.Angle} (hvs : inner ℝ v (normalVector s) = 0) (hvt : inner ℝ v (normalVector t) = 0) :

s = t ∨ s = t + ↑Real.pi

Two angular unit normals perpendicular to a nonzero planar vector are equal or antipodal.

source

theorem MovingSofa.segmentPresentation_measure_eq (K : ConvexBody Point) {d c : Point × Point × Real.Angle} (hd : IsSegmentPresentation K d) (hc : IsSegmentPresentation K c) :

ENNReal.ofReal (dist d.1 d.2.1) • (MeasureTheory.Measure.dirac d.2.2 + MeasureTheory.Measure.dirac (d.2.2 + ↑Real.pi)) = ENNReal.ofReal (dist c.1 c.2.1) • (MeasureTheory.Measure.dirac c.2.2 + MeasureTheory.Measure.dirac (c.2.2 + ↑Real.pi))

The atomic segment measure is independent of its segment presentation.

source

theorem MovingSofa.surfaceAreaMeasure_eq_zero_of_subsingleton (K : ConvexBody Point) (hK : (↑K).Subsingleton) :

surfaceAreaMeasure K = 0

A singleton convex body has zero surface measure.

source

theorem MovingSofa.not_subsingleton_of_isSegmentPresentation (K : ConvexBody Point) {d : Point × Point × Real.Angle} (hd : IsSegmentPresentation K d) :

¬(↑K).Subsingleton

A nondegenerate segment presentation makes the represented convex body nonsingleton.

source

theorem MovingSofa.surfaceAreaMeasure_eq_segmentPresentation (K : ConvexBody Point) (d : Point × Point × Real.Angle) (hd : IsSegmentPresentation K d) :

surfaceAreaMeasure K = ENNReal.ofReal (dist d.1 d.2.1) • (MeasureTheory.Measure.dirac d.2.2 + MeasureTheory.Measure.dirac (d.2.2 + ↑Real.pi))

The surface measure of a segment is its length times the two normal atoms.

source

theorem MovingSofa.isFiniteMeasure_surfaceAreaMeasure_of_subsingleton (K : ConvexBody Point) (hK : (↑K).Subsingleton) :

MeasureTheory.IsFiniteMeasure (surfaceAreaMeasure K)

The surface area measure of a singleton convex body is finite.

source

theorem MovingSofa.isFiniteMeasure_surfaceAreaMeasure_of_segmentPresentation (K : ConvexBody Point) {d : Point × Point × Real.Angle} (hd : IsSegmentPresentation K d) :

MeasureTheory.IsFiniteMeasure (surfaceAreaMeasure K)

The surface area measure of a convex body with a segment presentation is finite.

Analysis / Surface Measure / Segment Faces #

source

theorem MovingSofa.exposedEdge_eq_segment_of_orthogonal (K : ConvexBody Point) (d : Point × Point × Real.Angle) (hd : IsSegmentPresentation K d) (t : Real.Angle) (ht : inner ℝ (d.2.1 - d.1) (normalVector t) = 0) :

exposedEdge K t = ↑K

A normal perpendicular to a segment exposes the whole segment.

source

theorem MovingSofa.surfaceAreaMeasure_face_union_of_segmentPresentation (K : ConvexBody Point) (d : Point × Point × Real.Angle) (hd : IsSegmentPresentation K d) (E : Set Real.Angle) (hE : MeasurableSet E) {a b : ℝ} (hab : a ≤ b) (hshort : b < a + Real.pi) (hsubset : E ⊆ (fun (t : ℝ) => ↑t) '' Set.Icc a b) :

(surfaceAreaMeasure K) E = (MeasureTheory.Measure.hausdorffMeasure 1) (⋃ t ∈ E, exposedEdge K t)

The face-union formula for a segment on an angular arc shorter than a half-turn.

Analysis / Surface Measure / Segment Graph #

source

theorem MovingSofa.horizontalBounds_eq_of_subsingleton (K : ConvexBody Point) (hK : (↑K).Subsingleton) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) :

(horizontalBounds K o e).1 = (horizontalBounds K o e).2

A singleton convex body has equal horizontal projection bounds.

source

theorem MovingSofa.surfaceAreaMeasure_integral_eq_zero_of_subsingleton (K : ConvexBody Point) (hK : (↑K).Subsingleton) (ψ : Real.Angle → ℝ) :

∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure K = 0

Every surface-area integral of a singleton convex body vanishes.

source

theorem MovingSofa.segment_integral_eq_zero_of_horizontalBounds_eq (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) (ψ : Real.Angle → ℝ) (ε : ℝ) (hε : 0 < ε) (hsupport : ∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) (d : Point × Point × Real.Angle) (hd : IsSegmentPresentation K d) (hbounds : (horizontalBounds K o e).1 = (horizontalBounds K o e).2) :

∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure K = 0

A segment with zero horizontal width contributes zero against weights supported on normals with positive vertical coordinate.

source

theorem MovingSofa.segment_graph_formula (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ ] Point) (ψ : Real.Angle → ℝ) {ε : ℝ} (hε : 0 < ε) (hsupport : ∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) (d : Point × Point × Real.Angle) (hd : IsSegmentPresentation K d) (hbounds : (horizontalBounds K o e).1 < (horizontalBounds K o e).2) :

MeasureTheory.Integrable (upperGraphSurfaceIntegrand K o e ψ) (MeasureTheory.volume.restrict (Set.Icc (horizontalBounds K o e).1 (horizontalBounds K o e).2)) ∧ ∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure K = ∫ (x : ℝ) in Set.Icc (horizontalBounds K o e).1 (horizontalBounds K o e).2, upperGraphSurfaceIntegrand K o e ψ x

The surface-area integral of a nonvertical segment agrees with its upper graph integral.

source

theorem MovingSofa.exists_segmentPresentation_of_interior_empty (K : ConvexBody Point) (hsub : ¬(↑K).Subsingleton) (hint : interior ↑K = ∅) :

∃ (d : Point × Point × Real.Angle), IsSegmentPresentation K d

A nonsingleton planar convex body with empty interior has a segment presentation.

Curve.Foundations.Development001.

Curve.Area.
Curve.AreaTransport.
Curve.Concatenation.
Curve.AreaAdditivity.
Curve.CyclicRotation.
Curve.Jordan.Basic.
Curve.Jordan.Orientation.
Curve.Jordan.Area.
Curve.Jordan.ArcArea.
Curve.Jordan.Parametrization.
Curve.Jordan.UnitSphere.
Curve.Jordan.Winding.
Curve.Jordan.RadialWinding.
Curve.Jordan.WindingConcatenation.
Curve.Jordan.CyclicRotation.
Curve.Jordan.WindingKernel.
Curve.Jordan.WindingLocalConstancy.
Curve.Jordan.WindingLifts.
Curve.NullRange.
Curve.SegmentArea.
Curve.SegmentArea.Parametrization.
Curve.SmoothIntervalPaths.
Curve.Jordan.RadialLoop.
Curve.StieltjesChainRule.

Curve / Area #

source

def MovingSofa.constBVPath (a b : ℝ) (p : Point) :

ContinuousBVPaths a b

The constant planar path, as a continuous path of bounded variation.

Equations

MovingSofa.constBVPath a b p = ⟨fun (x : ↑(Set.Icc a b)) => p, ⋯⟩

Instances For

source

def MovingSofa.continuousBVCoordinate {a b : ℝ} (x : ContinuousBVPaths a b) (i : Fin 2) :

RightContinuousIntervalBV a b

View one coordinate of a continuous BV path as a right-continuous BV function.

Equations

MovingSofa.continuousBVCoordinate x i = { toFun := fun (t : ↑(Set.Icc a b)) => (↑x t).ofLp i, boundedVariation := ⋯, right_continuous := ⋯ }

Instances For

source

noncomputable def MovingSofa.curveAreaFunctional {a b : ℝ} (x : ContinuousBVPaths a b) :

ℝ

Half the difference of the two coordinate Stieltjes integrals, giving signed area.

Equations

One or more equations did not get rendered due to their size.

Instances For

Curve / Area Transport #

source

theorem MovingSofa.continuousBVPaths_comp_monotone_surjective {a b c d : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)) (hφc : Continuous φ) (hφm : Monotone φ) (hφs : Function.Surjective φ) :

∃ (y : ContinuousBVPaths c d), ↑y = ↑x ∘ φ

A continuous monotone surjection preserves continuous bounded variation.

source

theorem MovingSofa.curveArea_comp_monotone_surjective {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (x : ContinuousBVPaths a b) (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)) (hφc : Continuous φ) (hφm : Monotone φ) (hφs : Function.Surjective φ) :

∃ (y : ContinuousBVPaths c d), ↑y = ↑x ∘ φ ∧ curveAreaFunctional y = curveAreaFunctional x

A continuous monotone surjection preserves signed path area.

source

theorem MovingSofa.curveAreaFunctional_eq_of_comp_monotone_surjective {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (x : ContinuousBVPaths a b) (y : ContinuousBVPaths c d) (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)) (hφc : Continuous φ) (hφm : Monotone φ) (hφs : Function.Surjective φ) (hy : ↑y = ↑x ∘ φ) :

curveAreaFunctional y = curveAreaFunctional x

A continuous monotone surjective reparametrisation identifies the signed areas of two given paths whenever one is the composite of the other with it.

source

theorem MovingSofa.curveAreaFunctional_add_constBVPath {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (v : Point) :

curveAreaFunctional (x + constBVPath a b v) = curveAreaFunctional x + (v.ofLp 0 * ((↑x ⟨b, ⋯⟩).ofLp 1 - (↑x ⟨a, ⋯⟩).ofLp 1) - v.ofLp 1 * ((↑x ⟨b, ⋯⟩).ofLp 0 - (↑x ⟨a, ⋯⟩).ofLp 0)) / 2

Translating a continuous BV path shifts its signed area by the cross product of the translation vector with the path's total displacement, halved.

source

theorem MovingSofa.curveArea_comp_reverse {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) :

let r := Set.Icc.reverse hab; have y := ⟨↑x ∘ r, ⋯⟩; curveAreaFunctional y = -curveAreaFunctional x

Reversing a continuous BV path negates its signed area.

source

theorem MovingSofa.curveArea_comp_antitone_surjective {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (x : ContinuousBVPaths a b) (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)) (hφc : Continuous φ) (hφa : Antitone φ) (hφs : Function.Surjective φ) :

∃ (y : ContinuousBVPaths c d), ↑y = ↑x ∘ φ ∧ curveAreaFunctional y = -curveAreaFunctional x

A continuous antitone surjection negates signed path area.

source

theorem MovingSofa.curveAreaFunctional_eq_zero_of_constant {a b : ℝ} (x : ContinuousBVPaths a b) (p : Point) (hx : ∀ (t : ↑(Set.Icc a b)), ↑x t = p) :

curveAreaFunctional x = 0

A constant path has zero signed area, including on an empty parameter interval.

source

theorem MovingSofa.curveArea_comp_monotone_or_antitone_surjective {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) (x : ContinuousBVPaths a b) (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)) (hφc : Continuous φ) (hφs : Function.Surjective φ) (hφ : Monotone φ ∨ Antitone φ) :

∃ (y : ContinuousBVPaths c d), ↑y = ↑x ∘ φ ∧ (Monotone φ → curveAreaFunctional y = curveAreaFunctional x) ∧ (Antitone φ → curveAreaFunctional y = -curveAreaFunctional x)

A continuous monotone or antitone surjection transports BV paths and signed area.

Curve / Concatenation #

source

structure MovingSofa.RectifiablePathData :

Type

A continuous path of bounded variation with an ordered real parameter interval.

a : ℝ
The initial real parameter.
b : ℝ
The terminal real parameter.
ordered : self.a ≤ self.b
path : ContinuousBVPaths self.a self.b
The continuous parametrization of bounded variation.

Instances For

source

def MovingSofa.IsPathConcatenation (Γ : RectifiablePathData) {n : ℕ} (pieces : Fin n → RectifiablePathData) :

Prop

An ordered interval partition identifies the path with a nonempty list of parametrized pieces.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MovingSofa.IsPathConcatenation.range_subset_iUnion {Γ : RectifiablePathData} {n : ℕ} {pieces : Fin n → RectifiablePathData} (h : IsPathConcatenation Γ pieces) :

Set.range ↑Γ.path ⊆ ⋃ (i : Fin n), Set.range ↑(pieces i).path

A concatenated path stays inside the union of the ranges of its pieces.

Curve / Area Additivity #

source

theorem MovingSofa.curveArea_concatenation (Γ : RectifiablePathData) {n : ℕ} (pieces : Fin n → RectifiablePathData) (h : IsPathConcatenation Γ pieces) :

curveAreaFunctional Γ.path = ∑ i : Fin n, curveAreaFunctional (pieces i).path

Curve / Cyclic Rotation #

source

def MovingSofa.ContinuousBVPaths.restrict {a b : ℝ} (x : ContinuousBVPaths a b) (l u : ↑(Set.Icc a b)) (_hlu : l ≤ u) :

ContinuousBVPaths ↑l ↑u

Restrict a continuous BV path to a closed subinterval.

Equations

x.restrict l u _hlu = ⟨↑x ∘ fun (t : ↑(Set.Icc ↑l ↑u)) => ⟨↑t, ⋯⟩, ⋯⟩

Instances For

source

theorem MovingSofa.curveArea_eq_sum_restrict {a b : ℝ} (x : ContinuousBVPaths a b) {n : ℕ} (cuts : Fin (n + 1) → ↑(Set.Icc a b)) (hcuts : Monotone cuts) (hzero : ↑(cuts 0) = a) (hlast : ↑(cuts (Fin.last n)) = b) :

curveAreaFunctional x = ∑ i : Fin n, curveAreaFunctional (x.restrict (cuts i.castSucc) (cuts i.succ) ⋯)

Signed path area is additive along any monotone chain of cuts of the parameter interval.

source

theorem MovingSofa.curveArea_eq_restriction_add_restriction {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (s : ↑(Set.Icc a b)) :

let a' := ⟨a, ⋯⟩; let b' := ⟨b, ⋯⟩; curveAreaFunctional x = curveAreaFunctional (x.restrict a' s ⋯) + curveAreaFunctional (x.restrict s b' ⋯)

Split the signed area of a continuous BV path at any parameter value.

source

theorem MovingSofa.curveArea_cyclic_cut_sum {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (s : ↑(Set.Icc a b)) :

let a' := ⟨a, ⋯⟩; let b' := ⟨b, ⋯⟩; curveAreaFunctional x = curveAreaFunctional (x.restrict s b' ⋯) + curveAreaFunctional (x.restrict a' s ⋯)

The tail and head restrictions have signed areas summing to the original area.

source

def MovingSofa.ContinuousBVPaths.restrictionData {a b : ℝ} (x : ContinuousBVPaths a b) (l u : ↑(Set.Icc a b)) (hlu : l ≤ u) :

RectifiablePathData

Package a restricted continuous BV path with its interval endpoints.

Equations

x.restrictionData l u hlu = { a := ↑l, b := ↑u, ordered := hlu, path := x.restrict l u hlu }

Instances For

source

theorem MovingSofa.curveArea_cyclic_rotation {a b c d : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (s : ↑(Set.Icc a b)) (rotated : ContinuousBVPaths c d) (hcd : c ≤ d) (hrot : IsPathConcatenation { a := c, b := d, ordered := hcd, path := rotated } ![x.restrictionData s ⟨b, ⋯⟩ ⋯, x.restrictionData ⟨a, ⋯⟩ s ⋯]) :

curveAreaFunctional rotated = curveAreaFunctional x

A tail-then-head concatenation preserves the signed area.

source

theorem MovingSofa.boundedVariation_concatUnitIntervals_coordinate (p q : ContinuousBVPaths 0 1) (hjoin : ↑p ⟨1, boundedVariation_concatUnitIntervals_coordinate._proof_1 ⟩ = ↑q ⟨0, boundedVariation_concatUnitIntervals_coordinate._proof_2 ⟩) (i : Fin 2) :

BoundedVariationOn (fun (t : ↑(Set.Icc 0 2)) => (Function.concatUnitIntervals (↑p) (↑q) t).ofLp i) Set.univ

Concatenating continuous paths with matching endpoints preserves coordinatewise variation.

source

theorem MovingSofa.exists_cyclic_rotation_path {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (s : ↑(Set.Icc a b)) (hx : ↑x ⟨b, ⋯⟩ = ↑x ⟨a, ⋯⟩) :

∃ (rotated : ContinuousBVPaths 0 2), ↑rotated = Function.concatUnitIntervals (↑x ∘ Set.Icc.convexComb s ⟨b, ⋯⟩) (↑x ∘ Set.Icc.convexComb ⟨a, ⋯⟩ s) ∧ IsPathConcatenation { a := 0, b := 2, ordered := exists_cyclic_rotation_path._proof_1, path := rotated } ![x.restrictionData s ⟨b, ⋯⟩ ⋯, x.restrictionData ⟨a, ⋯⟩ s ⋯]

Rotate a closed continuous BV path by concatenating its tail and head.

source

theorem MovingSofa.exists_cyclic_rotation_eq_concat {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (s : ↑(Set.Icc a b)) (hx : ↑x ⟨b, ⋯⟩ = ↑x ⟨a, ⋯⟩) :

Construct an area-preserving cyclic rotation of a closed continuous BV path.

source

theorem MovingSofa.range_cyclic_concat {a b : ℝ} (hab : a ≤ b) (x : ↑(Set.Icc a b) → Point) (s : ↑(Set.Icc a b)) (hx : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) :

Set.range (Function.concatUnitIntervals (x ∘ Set.Icc.convexComb s ⟨b, ⋯⟩) (x ∘ Set.Icc.convexComb ⟨a, ⋯⟩ s)) = Set.range x

Cutting and rejoining a closed path does not change its carrier.

source

theorem MovingSofa.exists_param_lt_top_of_mem_range {a b : ℝ} (hab : a < b) (x : ↑(Set.Icc a b) → Point) (hx : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) {p : Point} (hp : p ∈ Set.range x) :

∃ (s : ↑(Set.Icc a b)), ↑s < b ∧ x s = p

Every point of a nondegenerate closed path occurs before its terminal parameter.

Curve / Jordan / Basic #

source

def MovingSofa.IsJordanArc (Γ : Set Point) :

Prop

The set is the range of an injective continuous map from a closed real interval.

Equations

MovingSofa.IsJordanArc Γ = ∃ (a : ℝ) (b : ℝ) (_ : a ≤ b) (x : ↑(Set.Icc a b) → MovingSofa.Point), Continuous x ∧ Function.Injective x ∧ Set.range x = Γ

Instances For

source

def MovingSofa.IsJordanCurve (Γ : Set Point) :

Prop

The set is the range of an injective continuous map from the circle.

Equations

MovingSofa.IsJordanCurve Γ = ∃ (x : Circle → MovingSofa.Point), Continuous x ∧ Function.Injective x ∧ Set.range x = Γ

Instances For

source

def MovingSofa.jordanSets :

(Set Point → Prop) × (Set Point → Prop)

Bundle the predicates for Jordan arcs and Jordan curves.

Equations

MovingSofa.jordanSets = (MovingSofa.IsJordanArc , MovingSofa.IsJordanCurve )

Instances For

source

def MovingSofa.IsOrientedJordanArc (Γ : Set Point) (p q : Point) :

Prop

A Jordan arc admits a parametrization with the specified starting and ending points.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure MovingSofa.OrientedJordanArc :

Type

A Jordan arc equipped with ordered endpoints.

carrier : Set Point
The point set traced by the arc.
startPoint : Point
The initial endpoint of the oriented arc.
endPoint : Point
The terminal endpoint of the oriented arc.
parametrizable : IsOrientedJordanArc self.carrier self.startPoint self.endPoint

Instances For

Curve / Jordan / Orientation #

source

def MovingSofa.jordanInterior (Γ : Set Point) :

Set Point

Points outside the curve whose connected component in its complement is bounded.

Equations

MovingSofa.jordanInterior Γ = {p : MovingSofa.Point | p ∉ Γ ∧ Bornology.IsBounded (connectedComponentIn Γᶜ p)}

Instances For

source

def MovingSofa.IsCurveAngleLift {a b : ℝ} (x : ↑(Set.Icc a b) → Point) (p : Point) (θ : ↑(Set.Icc a b) → ℝ) :

Prop

A continuous real angle lifts the normalized displacement from the specified point.

Equations

MovingSofa.IsCurveAngleLift x p θ = (Continuous θ ∧ ∀ (t : ↑(Set.Icc a b)), Real.cos (θ t) = (x t - p).ofLp 0 / ‖x t - p‖ ∧ Real.sin (θ t) = (x t - p).ofLp 1 / ‖x t - p‖)

Instances For

source

noncomputable def MovingSofa.curveWinding {a b : ℝ} (hab : a ≤ b) (x : ↑(Set.Icc a b) → Point) (p : Point) :

ℝ

The angle-lift increment divided by 2π, with value zero if no lift exists.

Equations

MovingSofa.curveWinding hab x p = if h : ∃ (θ : ↑(Set.Icc a b) → ℝ), MovingSofa.IsCurveAngleLift x p θ then (h.choose ⟨b, ⋯⟩ - h.choose ⟨a, ⋯⟩) / (2 * Real.pi) else 0

Instances For

source

def MovingSofa.IsOrientedJordanParametrization {a b : ℝ} (hab : a ≤ b) (Γ : Set Point) (counterclockwise : Bool) (x : ↑(Set.Icc a b) → Point) :

Prop

A simple closed parametrization with the specified winding sign on the interior.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure MovingSofa.OrientedJordanCurve :

Type

A Jordan curve together with a choice of clockwise or counterclockwise orientation.

carrier : Set Point
The point set traced by the Jordan curve.
isJordan : IsJordanCurve self.carrier
counterclockwise : Bool
Select positive winding orientation when true and negative orientation when false.

Instances For

source

noncomputable def MovingSofa.jordanCurveOrientation :

((a b : ℝ) → a ≤ b → (↑(Set.Icc a b) → Point) → Point → ℝ) × ((a b : ℝ) → a ≤ b → Set Point → Bool → (↑(Set.Icc a b) → Point) → Prop)

Bundle the winding functional and the oriented-parametrization predicate.

Equations

MovingSofa.jordanCurveOrientation = (fun (x x_1 : ℝ) (hab : x ≤ x_1) => MovingSofa.curveWinding hab, fun (x x_1 : ℝ) (hab : x ≤ x_1) => MovingSofa.IsOrientedJordanParametrization hab)

Instances For

Curve / Jordan / Area #

source

structure MovingSofa.ArcBVParametrization (Γ : OrientedJordanArc) :

Type

An injective continuous BV parametrization respecting an oriented arc’s endpoints.

a : ℝ
The initial real parameter.
b : ℝ
The terminal real parameter.
ordered : self.a ≤ self.b
path : ContinuousBVPaths self.a self.b
The continuous parametrization of bounded variation.
injective : Function.Injective ↑self.path
range_eq : Set.range ↑self.path = Γ.carrier
start_eq : ↑self.path ⟨self.a, ⋯⟩ = Γ.startPoint
end_eq : ↑self.path ⟨self.b, ⋯⟩ = Γ.endPoint

Instances For

source

structure MovingSofa.ClosedBVParametrization (Γ : OrientedJordanCurve) :

Type

A continuous BV parametrization respecting a Jordan curve’s orientation.

a : ℝ
The initial real parameter.
b : ℝ
The terminal real parameter.
ordered : self.a ≤ self.b
path : ContinuousBVPaths self.a self.b
The continuous parametrization of bounded variation.
oriented : IsOrientedJordanParametrization ⋯ Γ.carrier Γ.counterclockwise ↑self.path

Instances For

source

@[reducible, inline]

abbrev MovingSofa.RectifiableOrientedArc :

Type

Oriented Jordan arcs admitting a continuous BV parametrization.

Equations

MovingSofa.RectifiableOrientedArc = { Γ : MovingSofa.OrientedJordanArc // Nonempty (MovingSofa.ArcBVParametrization Γ) }

Instances For

source

@[reducible, inline]

abbrev MovingSofa.RectifiableOrientedCurve :

Type

Oriented Jordan curves admitting a continuous BV parametrization.

Equations

MovingSofa.RectifiableOrientedCurve = { Γ : MovingSofa.OrientedJordanCurve // Nonempty (MovingSofa.ClosedBVParametrization Γ) }

Instances For

source

noncomputable def MovingSofa.jordanArcArea (Γ : RectifiableOrientedArc) :

ℝ

The signed Stieltjes area of a chosen BV parametrization of the oriented arc.

Equations

MovingSofa.jordanArcArea Γ = MovingSofa.curveAreaFunctional (Classical.choice ⋯).path

Instances For

source

noncomputable def MovingSofa.jordanClosedCurveArea (Γ : RectifiableOrientedCurve) :

ℝ

The signed Stieltjes area of a chosen BV parametrization of the oriented curve.

Equations

MovingSofa.jordanClosedCurveArea Γ = MovingSofa.curveAreaFunctional (Classical.choice ⋯).path

Instances For

source

noncomputable def MovingSofa.jordanArea :

(RectifiableOrientedArc → ℝ) × (RectifiableOrientedCurve → ℝ)

Bundle the signed area functionals for oriented arcs and closed curves.

Equations

MovingSofa.jordanArea = (MovingSofa.jordanArcArea , MovingSofa.jordanClosedCurveArea )

Instances For

Curve / Jordan / Arc Area #

source

theorem MovingSofa.curveArea_arc_same_carrier (Γ Δ : OrientedJordanArc) (x : ArcBVParametrization Γ) (y : ArcBVParametrization Δ) (hcarrier : Γ.carrier = Δ.carrier) :

(Γ.startPoint = Δ.startPoint → Γ.endPoint = Δ.endPoint → curveAreaFunctional x.path = curveAreaFunctional y.path) ∧ (Γ.startPoint = Δ.endPoint → Γ.endPoint = Δ.startPoint → curveAreaFunctional x.path = -curveAreaFunctional y.path)

Same-carrier Jordan arcs have equal or opposite signed areas according to their endpoints.

Curve / Jordan / Parametrization #

source

def MovingSofa.openIntervalToIntervalInterior {a b : ℝ} (_hab : a < b) :

↑(Set.Ioo a b) ≃ₜ ↑{t : ↑(Set.Icc a b) | a < ↑t ∧ ↑t < b}

Identify an open interval with the corresponding subset of the closed interval.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def MovingSofa.intervalToRange {a b : ℝ} (x : ↑(Set.Icc a b) → Point) :

↑(Set.Icc a b) → ↑(Set.range x)

Regard a parametrized point as an element of the path’s range.

Equations

MovingSofa.intervalToRange x t = ⟨x t, ⋯⟩

Instances For

source

theorem MovingSofa.intervalToRange_continuous {a b : ℝ} (x : ↑(Set.Icc a b) → Point) (hx : Continuous x) :

Continuous (intervalToRange x)

source

theorem MovingSofa.intervalToRange_surjective {a b : ℝ} (x : ↑(Set.Icc a b) → Point) :

Function.Surjective (intervalToRange x)

source

def MovingSofa.puncturedLoopRangeSet {a b : ℝ} (hab : a ≤ b) (x : ↑(Set.Icc a b) → Point) :

Set ↑(Set.range x)

The carrier of a closed parametrized loop with its basepoint removed.

Equations

MovingSofa.puncturedLoopRangeSet hab x = {p : ↑(Set.range x) | ↑p ≠ x ⟨a, ⋯⟩}

Instances For

source

theorem MovingSofa.puncturedLoopRangeSet_isOpen {a b : ℝ} (hab : a ≤ b) (x : ↑(Set.Icc a b) → Point) :

IsOpen (puncturedLoopRangeSet hab x)

source

theorem MovingSofa.intervalToRange_preimage_punctured {a b : ℝ} (hab : a ≤ b) (hab' : a < b) (x : ↑(Set.Icc a b) → Point) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (hinj : Set.InjOn x {t : ↑(Set.Icc a b) | ↑t < b}) :

intervalToRange x ⁻¹' puncturedLoopRangeSet hab x = {t : ↑(Set.Icc a b) | a < ↑t ∧ ↑t < b}

source

theorem MovingSofa.intervalToPuncturedRange_injective {a b : ℝ} (hab : a ≤ b) (_hab' : a < b) (x : ↑(Set.Icc a b) → Point) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (hinj : Set.InjOn x {t : ↑(Set.Icc a b) | ↑t < b}) :

Function.Injective ((puncturedLoopRangeSet hab x).restrictPreimage (intervalToRange x))

source

noncomputable def MovingSofa.openIntervalHomeomorphPuncturedRange {a b : ℝ} (hab : a ≤ b) (hab' : a < b) (x : ↑(Set.Icc a b) → Point) (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (hinj : Set.InjOn x {t : ↑(Set.Icc a b) | ↑t < b}) :

↑(Set.Ioo a b) ≃ₜ ↑(puncturedLoopRangeSet hab x)

Removing the basepoint turns a closed once-traversal into a homeomorphism from the open parameter interval onto the punctured carrier.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem MovingSofa.openIntervalHomeomorphPuncturedRange_coe {a b : ℝ} (hab : a ≤ b) (hab' : a < b) (x : ↑(Set.Icc a b) → Point) (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (hinj : Set.InjOn x {t : ↑(Set.Icc a b) | ↑t < b}) (t : ↑(Set.Ioo a b)) :

↑↑((openIntervalHomeomorphPuncturedRange hab hab' x hx hclosed hinj) t) = x ⟨↑t, ⋯⟩

The punctured-loop homeomorphism agrees pointwise with the original path.

source

theorem MovingSofa.exists_reparametrization_of_range_eq_of_start_eq {a b c d : ℝ} (hab : a ≤ b) (hab' : a < b) (hcd : c ≤ d) (hcd' : c < d) (x : ↑(Set.Icc a b) → Point) (y : ↑(Set.Icc c d) → Point) (hxc : Continuous x) (hyc : Continuous y) (hxclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (hyclosed : y ⟨c, ⋯⟩ = y ⟨d, ⋯⟩) (hxinj : Set.InjOn x {t : ↑(Set.Icc a b) | ↑t < b}) (hyinj : Set.InjOn y {t : ↑(Set.Icc c d) | ↑t < d}) (hrange : Set.range x = Set.range y) (hstart : x ⟨a, ⋯⟩ = y ⟨c, ⋯⟩) :

∃ (φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)), Continuous φ ∧ Function.Surjective φ ∧ (Monotone φ ∨ Antitone φ) ∧ y = x ∘ φ

Equal-start simple closed paths with the same range admit a monotone or antitone transition.

source

theorem MovingSofa.ClosedBVParametrization.exists_reparametrization_of_start_eq {Γ Δ : OrientedJordanCurve} (x : ClosedBVParametrization Γ) (y : ClosedBVParametrization Δ) (hcarrier : Γ.carrier = Δ.carrier) (hstart : ↑x.path ⟨x.a, ⋯⟩ = ↑y.path ⟨y.a, ⋯⟩) :

∃ (φ : ↑(Set.Icc y.a y.b) → ↑(Set.Icc x.a x.b)), Continuous φ ∧ Function.Surjective φ ∧ (Monotone φ ∨ Antitone φ) ∧ ↑y.path = ↑x.path ∘ φ

Equal-start closed Jordan parametrizations admit a monotone or antitone transition.

Curve / Jordan / Unit Sphere #

source

theorem MovingSofa.isJordanCurve_of_unitSphere_homeomorph {Γ : Set Point} (e : ↑{u : Point | ‖u‖ = 1} ≃ₜ ↑Γ) :

IsJordanCurve Γ

A planar set homeomorphic to the unit sphere is a Jordan curve.

Curve / Jordan / Winding #

source

theorem MovingSofa.IsCurveAngleLift.endpoint_increment_eq {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} {p : Point} {θ ψ : ↑(Set.Icc a b) → ℝ} (hθ : IsCurveAngleLift x p θ) (hψ : IsCurveAngleLift x p ψ) :

θ ⟨b, ⋯⟩ - θ ⟨a, ⋯⟩ = ψ ⟨b, ⋯⟩ - ψ ⟨a, ⋯⟩

Two continuous angle lifts have the same endpoint increment.

source

theorem MovingSofa.IsCurveAngleLift.curveWinding_eq {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} {p : Point} {θ : ↑(Set.Icc a b) → ℝ} (hθ : IsCurveAngleLift x p θ) :

curveWinding hab x p = (θ ⟨b, ⋯⟩ - θ ⟨a, ⋯⟩) / (2 * Real.pi)

Compute the winding value from any continuous angle lift.

source

theorem MovingSofa.exists_curveAngleLift_of_curveWinding_ne_zero {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} {p : Point} (h : curveWinding hab x p ≠ 0) :

∃ (θ : ↑(Set.Icc a b) → ℝ), IsCurveAngleLift x p θ

A nonzero winding value provides a continuous angle lift.

source

theorem MovingSofa.IsCurveAngleLift.comp {a b c d : ℝ} {x : ↑(Set.Icc a b) → Point} {p : Point} {θ : ↑(Set.Icc a b) → ℝ} (hθ : IsCurveAngleLift x p θ) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφ : Continuous φ) :

IsCurveAngleLift (x ∘ φ) p (θ ∘ φ)

Pull back an angle lift along a continuous parameter map.

source

theorem MovingSofa.IsCurveAngleLift.curveWinding_comp {a b c d : ℝ} (hcd : c ≤ d) {x : ↑(Set.Icc a b) → Point} {p : Point} {θ : ↑(Set.Icc a b) → ℝ} (hθ : IsCurveAngleLift x p θ) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφ : Continuous φ) :

curveWinding hcd (x ∘ φ) p = (θ (φ ⟨d, ⋯⟩) - θ (φ ⟨c, ⋯⟩)) / (2 * Real.pi)

Compute winding after continuous reparametrization from lifted endpoint values.

source

theorem MovingSofa.curveWinding_comp_of_endpoints {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {x : ↑(Set.Icc a b) → Point} {p : Point} (hx : ∃ (θ : ↑(Set.Icc a b) → ℝ), IsCurveAngleLift x p θ) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφ : Continuous φ) (hφa : φ ⟨c, ⋯⟩ = ⟨a, ⋯⟩) (hφb : φ ⟨d, ⋯⟩ = ⟨b, ⋯⟩) :

curveWinding hcd (x ∘ φ) p = curveWinding hab x p

A continuous reparametrization preserving endpoints preserves winding.

source

theorem MovingSofa.curveWinding_comp_of_reversed_endpoints {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {x : ↑(Set.Icc a b) → Point} {p : Point} (hx : ∃ (θ : ↑(Set.Icc a b) → ℝ), IsCurveAngleLift x p θ) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφ : Continuous φ) (hφa : φ ⟨c, ⋯⟩ = ⟨b, ⋯⟩) (hφb : φ ⟨d, ⋯⟩ = ⟨a, ⋯⟩) :

curveWinding hcd (x ∘ φ) p = -curveWinding hab x p

A continuous reparametrization exchanging endpoints negates winding.

Curve / Jordan / Radial Winding #

source

theorem MovingSofa.isCurveAngleLift_radial {a b : ℝ} (o : Point) (r : ↑(Set.Icc a b) → ℝ) (hr : ∀ (t : ↑(Set.Icc a b)), 0 < r t) :

IsCurveAngleLift (fun (t : ↑(Set.Icc a b)) => o + r t • normalVector ↑↑t) o fun (t : ↑(Set.Icc a b)) => ↑t

The parameter angle lifts a positive radial loop about its center.

source

theorem MovingSofa.curveWinding_radial_center (o : Point) (r : ↑(Set.Icc 0 (2 * Real.pi)) → ℝ) (hr : ∀ (t : ↑(Set.Icc 0 (2 * Real.pi))), 0 < r t) :

curveWinding curveWinding_radial_center._proof_1 (fun (t : ↑(Set.Icc 0 (2 * Real.pi))) => o + r t • normalVector ↑↑t) o = 1

A positive radial loop winds once around its center.

Curve / Jordan / Winding Concatenation #

source

theorem MovingSofa.curveWinding_concatUnitIntervals {x y : ↑(Set.Icc 0 1) → Point} {p : Point} {θ ψ : ↑(Set.Icc 0 1) → ℝ} (hθ : IsCurveAngleLift x p θ) (hψ : IsCurveAngleLift y p ψ) (hjoin : x ⟨1, boundedVariation_concatUnitIntervals_coordinate._proof_1 ⟩ = y ⟨0, boundedVariation_concatUnitIntervals_coordinate._proof_2 ⟩) :

curveWinding exists_cyclic_rotation_path._proof_1 (Function.concatUnitIntervals x y) p = curveWinding curveWinding_concatUnitIntervals._proof_1 x p + curveWinding curveWinding_concatUnitIntervals._proof_1 y p

Winding is additive for two paths joined at a common endpoint.

source

theorem MovingSofa.curveWinding_concat_of_cyclic_endpoints {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} {p : Point} {θ : ↑(Set.Icc a b) → ℝ} (hθ : IsCurveAngleLift x p θ) (hx : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (s : ↑(Set.Icc a b)) (φ ψ : ↑(Set.Icc 0 1) → ↑(Set.Icc a b)) (hφ : Continuous φ) (hψ : Continuous ψ) (hφ₀ : φ ⟨0, boundedVariation_concatUnitIntervals_coordinate._proof_2 ⟩ = s) (hφ₁ : φ ⟨1, boundedVariation_concatUnitIntervals_coordinate._proof_1 ⟩ = ⟨b, ⋯⟩) (hψ₀ : ψ ⟨0, boundedVariation_concatUnitIntervals_coordinate._proof_2 ⟩ = ⟨a, ⋯⟩) (hψ₁ : ψ ⟨1, boundedVariation_concatUnitIntervals_coordinate._proof_1 ⟩ = s) :

curveWinding exists_cyclic_rotation_path._proof_1 (Function.concatUnitIntervals (x ∘ φ) (x ∘ ψ)) p = curveWinding hab x p

Moving a closed path's cut point preserves winding.

Curve / Jordan / Cyclic Rotation #

source

theorem MovingSofa.exists_oriented_cyclic_rotation {a b : ℝ} (hab : a ≤ b) {Γ : Set Point} {ccw : Bool} (x : ContinuousBVPaths a b) (hx : IsOrientedJordanParametrization hab Γ ccw ↑x) (s : ↑(Set.Icc a b)) (has : a < ↑s) (hsb : ↑s < b) :

∃ (r : ContinuousBVPaths 0 2), IsOrientedJordanParametrization exists_cyclic_rotation_path._proof_1 Γ ccw ↑r ∧ ↑r ⟨0, exists_oriented_cyclic_rotation._proof_1 ⟩ = ↑x s ∧ curveAreaFunctional r = curveAreaFunctional x

Moving an oriented Jordan path's start to an interior parameter preserves area and orientation.

source

theorem MovingSofa.exists_oriented_cyclic_rotation_eq_concat {a b : ℝ} (hab : a ≤ b) {Γ : Set Point} {ccw : Bool} (x : ContinuousBVPaths a b) (hx : IsOrientedJordanParametrization hab Γ ccw ↑x) (s : ↑(Set.Icc a b)) (has : a < ↑s) (hsb : ↑s < b) :

∃ (r : ContinuousBVPaths 0 2), IsOrientedJordanParametrization exists_cyclic_rotation_path._proof_1 Γ ccw ↑r ∧ ↑r = Function.concatUnitIntervals (↑x ∘ Set.Icc.convexComb s ⟨b, ⋯⟩) (↑x ∘ Set.Icc.convexComb ⟨a, ⋯⟩ s)

A cyclic rotation together with its literal tail-then-head formula.

Curve / Jordan / Winding Kernel #

source

noncomputable def MovingSofa.windingKernel (z p : Point) :

Point

The inverse-distance vector kernel based at z.

Equations

MovingSofa.windingKernel z p = (‖z - p‖ ^ 2)⁻¹ • (z - p)

Instances For

source

theorem MovingSofa.integrableOn_windingKernel_ball (R : ℝ) (z : Point) (hz : ‖z‖ < R) :

MeasureTheory.IntegrableOn (windingKernel z) (Metric.ball 0 R) MeasureTheory.volume

The winding kernel is integrable on a disk containing its base point.

source

theorem MovingSofa.setIntegral_norm_windingKernel_ball_le (R : ℝ) (hR : 0 < R) (z : Point) (hz : ‖z‖ < R) :

∫ (p : Point) in Metric.ball 0 R, ‖windingKernel z p‖ ≤ 4 * Real.pi * R

The norm of the winding kernel has an integrable uniform majorant on an interior disk.

source

theorem MovingSofa.setIntegral_windingKernel_ball (R : ℝ) (z : Point) (hz : ‖z‖ < R) :

∫ (p : Point) in Metric.ball 0 R, windingKernel z p = Real.pi • z

The integral of the winding kernel over a disk is π times its base point.

source

theorem MovingSofa.windingKernel_coord_continuous_bounded {a b : ℝ} {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) {p : Point} (hp : p ∉ Set.range x) (i : Fin 2) :

(Continuous fun (t : ↑(Set.Icc a b)) => (windingKernel (x t) p).ofLp i) ∧ ∃ (C : ℝ), ∀ (t : ↑(Set.Icc a b)), |(windingKernel (x t) p).ofLp i| ≤ C

Off the range of a continuous interval path, each coordinate of the winding kernel is a bounded continuous function of the parameter.

Curve / Jordan / Winding Local Constancy #

source

theorem MovingSofa.continuous_arg_conj_mul_of_re_pos {α : Type u_1} [TopologicalSpace α] {z w : α → ℂ} (hz : Continuous z) (hw : Continuous w) (hpos : ∀ (t : α), 0 < ((starRingEnd ℂ) (z t) * w t).re) :

Continuous fun (t : α) => ((starRingEnd ℂ) (z t) * w t).arg

The principal relative argument varies continuously while the relative dot product is positive. This is the branch needed for a small displacement of the basepoint.

source

theorem MovingSofa.normalized_complex_rotation_by_arg {z w : ℂ} (hz : z ≠ 0) (hw : w ≠ 0) :

Real.cos (z.arg + ((starRingEnd ℂ) z * w).arg) = w.re / ‖w‖ ∧ Real.sin (z.arg + ((starRingEnd ℂ) z * w).arg) = w.im / ‖w‖

The principal relative argument rotates the normalized coordinates of z to those of w.

source

theorem MovingSofa.normalized_complex_rotation_by_relative_arg {z w : ℂ} {θ : ℝ} (hz : z ≠ 0) (hw : w ≠ 0) (hc : Real.cos θ = z.re / ‖z‖) (hs : Real.sin θ = z.im / ‖z‖) :

Real.cos (θ + ((starRingEnd ℂ) z * w).arg) = w.re / ‖w‖ ∧ Real.sin (θ + ((starRingEnd ℂ) z * w).arg) = w.im / ‖w‖

Coordinate form of the preceding rotation identity for any chosen real lift of z.

source

theorem MovingSofa.IsCurveAngleLift.add_principal_basepoint_correction {a b : ℝ} {x : ↑(Set.Icc a b) → Point} {p q : Point} {θ : ↑(Set.Icc a b) → ℝ} (hx : Continuous x) (hθ : IsCurveAngleLift x p θ) (hpos : ∀ (u : ↑(Set.Icc a b)), 0 < ((starRingEnd ℂ) (Complex.orthonormalBasisOneI.repr.symm (x u - p)) * Complex.orthonormalBasisOneI.repr.symm (x u - q)).re) :

IsCurveAngleLift x q fun (u : ↑(Set.Icc a b)) => θ u + ((starRingEnd ℂ) (Complex.orthonormalBasisOneI.repr.symm (x u - p)) * Complex.orthonormalBasisOneI.repr.symm (x u - q)).arg

A positive relative dot product supplies the continuous principal correction between two basepoints.

source

theorem MovingSofa.curveWinding_eq_of_relative_dot_pos {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) {p q : Point} {θ : ↑(Set.Icc a b) → ℝ} (hθ : IsCurveAngleLift x p θ) (hpos : ∀ (u : ↑(Set.Icc a b)), 0 < ((starRingEnd ℂ) (Complex.orthonormalBasisOneI.repr.symm (x u - p)) * Complex.orthonormalBasisOneI.repr.symm (x u - q)).re) :

curveWinding hab x q = curveWinding hab x p

Moving the basepoint through the positive-relative-dot neighborhood preserves winding.

source

theorem MovingSofa.exists_ball_relative_dot_pos {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) {p : Point} (hp : p ∉ Set.range x) :

∃ r > 0, ∀ (q : Point), dist q p < r → ∀ (u : ↑(Set.Icc a b)), 0 < ((starRingEnd ℂ) (Complex.orthonormalBasisOneI.repr.symm (x u - p)) * Complex.orthonormalBasisOneI.repr.symm (x u - q)).re

Off a compact continuous loop, every sufficiently nearby basepoint has positive relative dot product with the original radial vectors.

source

theorem MovingSofa.curveWinding_locally_constant_off_range {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) {p : Point} (hp : p ∉ Set.range x) :

∃ (U : Set Point), IsOpen U ∧ p ∈ U ∧ ∀ q ∈ U, curveWinding hab x q = curveWinding hab x p

Winding of a continuous closed loop is locally constant away from its range.

source

theorem MovingSofa.IsCurveAngleLift.sub_eq_arctan_of_dot_pos {a b : ℝ} {x : ↑(Set.Icc a b) → Point} {p : Point} {θ : ↑(Set.Icc a b) → ℝ} (hx : Continuous x) (hθ : IsCurveAngleLift x p θ) {t u : ↑(Set.Icc a b)} (htu : ↑t ≤ ↑u) (hpos : ∀ (s : ↑(Set.Icc a b)), ↑t ≤ ↑s → ↑s ≤ ↑u → 0 < (x t - p).ofLp 0 * (x s - p).ofLp 0 + (x t - p).ofLp 1 * (x s - p).ofLp 1) :

θ u - θ t = Real.arctan (((x t - p).ofLp 0 * (x u - p).ofLp 1 - (x t - p).ofLp 1 * (x u - p).ofLp 0) / ((x t - p).ofLp 0 * (x u - p).ofLp 0 + (x t - p).ofLp 1 * (x u - p).ofLp 1))

While the relative dot product with the initial radius vector stays positive, the increment of a continuous angle lift is the principal relative argument, computed as the arctangent of the ratio of the relative cross product to the relative dot product.

source

theorem MovingSofa.curveWinding_locally_constant_on_compl_range {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) {p : Point} (hp : p ∉ Set.range x) :

∃ (U : Set Point), IsOpen U ∧ p ∈ U ∧ ∀ q ∈ U, q ∉ Set.range x ∧ curveWinding hab x q = curveWinding hab x p

Winding is constant on an open neighbourhood of any point off the range of a closed continuous loop, and that neighbourhood avoids the range.

Curve / Jordan / Winding Lifts #

source

theorem MovingSofa.exists_curveAngleLift_of_avoids {a b : ℝ} (hab : a < b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) {p : Point} (hp : p ∉ Set.range x) :

∃ (α : ↑(Set.Icc a b) → ℝ), IsCurveAngleLift x p α

Every continuous interval path avoiding a point admits a continuous angle lift.

source

theorem MovingSofa.curveWinding_eq_zero_of_inner_pos {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (p v : Point) (hv : v ≠ 0) (hpos : ∀ (u : ↑(Set.Icc a b)), 0 < inner ℝ v (x u - p)) :

curveWinding hab x p = 0

A closed path contained in a strict half-plane about a point has winding zero there.

source

theorem MovingSofa.curveWinding_eq_zero_of_unbounded_component {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → Point} (hx : Continuous x) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) {p : Point} (hp : p ∉ Set.range x) (hunbounded : ¬Bornology.IsBounded (connectedComponentIn (Set.range x)ᶜ p)) :

curveWinding hab x p = 0

A closed continuous loop has winding zero at every point of an unbounded connected component of the complement of its range.

The range of an almost injective continuous BV path is null #

A continuous planar BV path that is injective on [a, b) sweeps a Lebesgue null set: each compact initial subarc has finite Hausdorff length, hence vanishing Hausdorff 2-measure, and a rational exhaustion together with the terminal point covers the whole range.

source

theorem MovingSofa.ContinuousBVPaths.volume_range_eq_zero_of_injOn {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (hinj : Set.InjOn ↑x {t : ↑(Set.Icc a b) | ↑t < b}) :

MeasureTheory.volume (Set.range ↑x) = 0

The range of a continuous planar BV path injective on [a, b) is Lebesgue null.

Curve / Segment Area #

source

noncomputable def MovingSofa.segmentArea (p q : Point) :

ℝ

Half the oriented determinant of the two endpoints.

Equations

MovingSofa.segmentArea p q = MovingSofa.planeCrossProduct p q / 2

Instances For

source

theorem MovingSofa.segmentArea_swap (p q : Point) :

segmentArea p q = -segmentArea q p

The signed segment area is antisymmetric in its two endpoints.

source

theorem MovingSofa.segmentArea_add_right (p q v : Point) :

segmentArea (p + v) (q + v) = segmentArea p q + (v.ofLp 0 * (q.ofLp 1 - p.ofLp 1) - v.ofLp 1 * (q.ofLp 0 - p.ofLp 0)) / 2

Translating both endpoints of a segment shifts its signed area by a boundary term.

source

theorem MovingSofa.segmentArea_combination_of_apply_one_eq (c : ℝ) {p₁ p₂ q₁ q₂ : Point} (hp : p₁.ofLp 1 = p₂.ofLp 1) (hq : q₁.ofLp 1 = q₂.ofLp 1) :

segmentArea ((1 - c) • p₁ + c • p₂) ((1 - c) • q₁ + c • q₂) = (1 - c) * segmentArea p₁ q₁ + c * segmentArea p₂ q₂

The signed area of the segment joining two convex combinations of endpoints is the same combination of the two signed areas, provided the two endpoints of each pair have a common height: the mixed terms then cancel.

source

theorem MovingSofa.segmentArea_eq_zero_of_inner_normalVector_eq_zero {p q : Point} {t : ℝ} (hp : inner ℝ p (normalVector ↑t) = 0) (hq : inner ℝ q (normalVector ↑t) = 0) :

segmentArea p q = 0

Two points on a normal line through the origin span no signed area.

source

theorem MovingSofa.segmentArea_sub_segmentArea_of_inner_normalVector_eq {p q s : Point} {t c : ℝ} (hp : inner ℝ p (normalVector ↑t) = c) (hq : inner ℝ q (normalVector ↑t) = c) (hs : inner ℝ s (normalVector ↑t) = c) :

segmentArea p s - segmentArea q s = segmentArea p q

Collinear additivity of the signed segment area on a common normal line.

Curve / Segment Area / Parametrization #

source

def MovingSofa.lineSegmentBVPath (p q : Point) :

ContinuousBVPaths 0 1

The affine segment from p to q, bundled as a continuous BV path.

Equations

MovingSofa.lineSegmentBVPath p q = ⟨⇑(Path.segment p q), ⋯⟩

Instances For

source

theorem MovingSofa.lineSegmentBVPath_apply (p q : Point) (s : ↑(Set.Icc 0 1)) :

↑(lineSegmentBVPath p q) s = (1 - ↑s) • p + ↑s • q

The affine parametrization of an oriented segment, evaluated.

source

theorem MovingSofa.curveAreaFunctional_lineSegmentBVPath (p q : Point) :

curveAreaFunctional (lineSegmentBVPath p q) = segmentArea p q

Curve / Smooth Interval Paths #

source

def MovingSofa.continuousBVOfContDiffOn {a b : ℝ} (f : ℝ → Point) (hf : ContDiffOn ℝ 1 f (Set.Icc a b)) :

ContinuousBVPaths a b

A continuously differentiable planar path on a compact interval has continuous bounded-variation coordinates.

Equations

MovingSofa.continuousBVOfContDiffOn f hf = ⟨fun (t : ↑(Set.Icc a b)) => f ↑t, ⋯⟩

Instances For

source

def MovingSofa.continuousBVOfLipschitz {a b : ℝ} (f : ↑(Set.Icc a b) → Point) {C : NNReal} (hf : LipschitzWith C f) :

ContinuousBVPaths a b

A Lipschitz planar path on a compact interval has continuous bounded-variation coordinates.

Equations

MovingSofa.continuousBVOfLipschitz f hf = ⟨f, ⋯⟩

Instances For

source

theorem MovingSofa.boundedVariationOn_coord_Icc_of_contDiffOn {a b : ℝ} (g : ↑(Set.Icc a b) → Point) {l r : ℝ} (hl : a ≤ l) (hlr : l ≤ r) (hr : r ≤ b) {F : ℝ → Point} (hF : ContDiffOn ℝ 1 F (Set.Icc l r)) (hgF : ∀ (t : ↑(Set.Icc l r)), g ⟨↑t, ⋯⟩ = F ↑t) (i : Fin 2) :

BoundedVariationOn (fun (t : ↑(Set.Icc a b)) => (g t).ofLp i) (Set.Icc ⟨l, ⋯⟩ ⟨r, ⋯⟩)

A coordinate of an interval path has bounded variation on a closed subinterval on which the path agrees with a continuously differentiable function.

source

def MovingSofa.continuousBVOfContDiffOnIccUnionIcc {a b c : ℝ} (f : ℝ → Point) (hab : a ≤ b) (hbc : b ≤ c) (h₁ : ContDiffOn ℝ 1 f (Set.Icc a b)) (h₂ : ContDiffOn ℝ 1 f (Set.Icc b c)) :

ContinuousBVPaths a c

Gluing two continuously differentiable pieces along a shared endpoint gives a continuous path of bounded variation.

Equations

MovingSofa.continuousBVOfContDiffOnIccUnionIcc f hab hbc h₁ h₂ = ⟨fun (t : ↑(Set.Icc a c)) => f ↑t, ⋯⟩

Instances For

Curve / Jordan / Radial Loop #

source

noncomputable def MovingSofa.radialBVLoop (f : ↑{u : Point | ‖u‖ = 1} → Point) {C : NNReal} (hf : LipschitzWith C f) :

ContinuousBVPaths 0 (2 * Real.pi)

A Lipschitz map on the unit circle induces a continuous BV loop in increasing angular order.

Equations

MovingSofa.radialBVLoop f hf = MovingSofa.continuousBVOfLipschitz (f ∘ fun (t : ↑(Set.Icc 0 (2 * Real.pi))) => ⟨MovingSofa.normalVector ↑↑t, ⋯⟩) ⋯

Instances For

source

theorem MovingSofa.radialBVLoop_apply (f : ↑{u : Point | ‖u‖ = 1} → Point) {C : NNReal} (hf : LipschitzWith C f) (t : ↑(Set.Icc 0 (2 * Real.pi))) :

↑(radialBVLoop f hf) t = f ⟨normalVector ↑↑t, ⋯⟩

The radial BV loop evaluates by applying the circle map to the angular normal.

source

theorem MovingSofa.radialBVLoop_closed (f : ↑{u : Point | ‖u‖ = 1} → Point) {C : NNReal} (hf : LipschitzWith C f) :

↑(radialBVLoop f hf) ⟨0, ⋯⟩ = ↑(radialBVLoop f hf) ⟨2 * Real.pi, ⋯⟩

The radial BV loop has equal endpoints.

source

theorem MovingSofa.radialBVLoop_injOn (f : ↑{u : Point | ‖u‖ = 1} → Point) {C : NNReal} (hf : LipschitzWith C f) (hinj : Function.Injective f) :

Set.InjOn ↑(radialBVLoop f hf) {t : ↑(Set.Icc 0 (2 * Real.pi)) | ↑t < 2 * Real.pi }

An injective circle map gives a radial loop injective before its final endpoint.

source

theorem MovingSofa.range_radialBVLoop (f : ↑{u : Point | ‖u‖ = 1} → Point) {C : NNReal} (hf : LipschitzWith C f) :

Set.range ↑(radialBVLoop f hf) = Set.range f

The radial BV loop has the same range as the underlying unit-circle map.

A Stieltjes chain rule with a local quadratic remainder #

The hypothesis of ContinuousBVPaths.stieltjes_chain_rule_of_local_quadratic_remainder quantifies the remainder only over parameter pairs closer than a fixed positive threshold. This is what a locally defined argument branch supplies: no single plane function has to be named, and no constant is needed across a branch cut.

source

theorem MovingSofa.ContinuousBVPaths.stieltjes_chain_rule_of_local_quadratic_remainder {a b : ℝ} (hab : a ≤ b) (x : ContinuousBVPaths a b) (hBV : BoundedVariationOn (↑x) Set.univ) (A : ↑(Set.Icc a b) → ℝ) (D : Point → Fin 2 → ℝ) (hD : ∀ (i : Fin 2), Continuous fun (t : ↑(Set.Icc a b)) => D (↑x t) i) {C : ℝ} (hC : 0 ≤ C) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (herror : ∀ (t u : ↑(Set.Icc a b)), ↑t ≤ ↑u → ↑u - ↑t < δ₀ → |A u - A t - (D (↑x t) 1 * ((↑x u).ofLp 1 - (↑x t).ofLp 1) - D (↑x t) 0 * ((↑x u).ofLp 0 - (↑x t).ofLp 0))| ≤ C * ‖↑x u - ↑x t‖ ^ 2) :

A ⟨b, ⋯⟩ - A ⟨a, ⋯⟩ = intervalStieltjesIntegral (continuousBVCoordinate x 1) (fun (t : ↑(Set.Icc a b)) => D (↑x t) 1) Set.univ - intervalStieltjesIntegral (continuousBVCoordinate x 0) (fun (t : ↑(Set.Icc a b)) => D (↑x t) 0) Set.univ

If a real parameter function A has increments matching the signed pair D₁ dγ₁ - D₀ dγ₀ up to a quadratic remainder on all parameter pairs closer than a fixed positive threshold, then its endpoint increment is the corresponding difference of coordinate Stieltjes integrals.

Area.Foundations.Development002.

Area.MonotoneRoof.
Area.ThreePieceRoof.

Area / Monotone Roof #

source

noncomputable def MovingSofa.monotoneRoofHeight {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) (s : ℝ) :

ℝ

Recover the vertical coordinate using a chosen inverse of the path’s horizontal coordinate.

Equations

MovingSofa.monotoneRoofHeight hab γ s = (↑γ (Function.invFun (fun (t : ↑(Set.Icc a b)) => (↑γ t).ofLp 0) s)).ofLp 1

Instances For

source

def MovingSofa.monotoneRoofRegion {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) :

Set Point

The closed region between the horizontal axis and the path’s roof graph.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MovingSofa.monotoneRoofLoop {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) (s : ↑(Set.Icc 0 2)) :

Point

Traverse the roof path backwards and return along its horizontal base.

Equations

MovingSofa.monotoneRoofLoop hab γ s = if hs : ↑s ≤ 1 then ↑γ ⟨b - (b - a) * ↑s, ⋯⟩ else (2 - ↑s) • ↑γ ⟨a, ⋯⟩ + (↑s - 1) • ↑γ ⟨b, ⋯⟩

Instances For

source

theorem MovingSofa.monotone_roof_signed_area {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) (hk : StrictMono fun (t : ↑(Set.Icc a b)) => (↑γ t).ofLp 0) (hh : ∀ (t : ↑(Set.Icc a b)), 0 ≤ (↑γ t).ofLp 1) (ha : (↑γ ⟨a, ⋯⟩).ofLp 1 = 0) (hb : (↑γ ⟨b, ⋯⟩).ofLp 1 = 0) :

∃ (Γ : ContinuousBVPaths 0 2), ↑Γ = monotoneRoofLoop hab γ ∧ curveAreaFunctional Γ = ClassicalResults.area (monotoneRoofRegion hab γ) ∧ ClassicalResults.area (monotoneRoofRegion hab γ) = ∫ (s : ℝ) in (↑γ ⟨a, ⋯⟩).ofLp 0..(↑γ ⟨b, ⋯⟩).ofLp 0, monotoneRoofHeight hab γ s

source

theorem MovingSofa.monotoneRoofHeight_apply {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) (hk : StrictMono fun (t : ↑(Set.Icc a b)) => (↑γ t).ofLp 0) (s : ↑(Set.Icc a b)) :

monotoneRoofHeight hab γ ((↑γ s).ofLp 0) = (↑γ s).ofLp 1

Above a parameter's abscissa, a strictly monotone roof has that parameter's ordinate.

source

theorem MovingSofa.exists_eq_monotoneRoof_fst {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) {c : ℝ} (hc : c ∈ Set.Icc ((↑γ ⟨a, ⋯⟩).ofLp 0) ((↑γ ⟨b, ⋯⟩).ofLp 0)) :

∃ (s : ↑(Set.Icc a b)), (↑γ s).ofLp 0 = c

Every abscissa between a roof's endpoints is the abscissa of a roof parameter.

source

theorem MovingSofa.monotoneRoofRegion_eq_param {a b : ℝ} (hab : a < b) (γ : ContinuousBVPaths a b) (hk : StrictMono fun (t : ↑(Set.Icc a b)) => (↑γ t).ofLp 0) :

monotoneRoofRegion hab γ = {p : Point | ∃ (s : ↑(Set.Icc a b)), p.ofLp 0 = (↑γ s).ofLp 0 ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ (↑γ s).ofLp 1}

The closed region under a strictly monotone roof, described parametrically: it consists of the points on or below the roof on the vertical line through some roof parameter.

Three-piece monotone roofs #

A three-piece roof over [r, l] is the continuous BV path on [0, 3] that runs up a straight segment from a base point P to f l, traverses an arc f backwards from l to r, and runs down a straight segment from f r to a base point Q. When the arc's first coordinate is strictly decreasing and P, Q lie strictly to the left of f l resp. to the right of f r, the resulting path has strictly increasing first coordinate, so it is a monotone roof in the sense of MovingSofa.monotoneRoofRegion.

area_region_under_strictMono_roof computes the area of the closed region under such a roof, above the base line y = -h carrying P and Q, as the signed area of the four-piece closed loop that bounds it, and area_region_under_roof_le compares that area with the areas of a base set and of a set containing the rest of the open region.

source

theorem MovingSofa.mem_Icc_roofArcTime {r l : ℝ} (hrl : r < l) {s : ℝ} (hs1 : 1 ≤ s) (hs2 : s ≤ 2) :

l + (s - 1) * (r - l) ∈ Set.Icc r l

The middle arc's parameter times run over the arc's own interval.

source

theorem MovingSofa.exists_strictMono_roof_of_strictAntiOn {r l : ℝ} (hrl : r < l) (c : ContinuousBVPaths r l) (f : ℝ → Point) (P Q : Point) (hf : ∀ (t : ℝ) (ht : t ∈ Set.Icc r l), ↑c ⟨t, ht⟩ = f t) (hanti : StrictAntiOn (fun (t : ℝ) => (f t).ofLp 0) (Set.Icc r l)) (hP : P.ofLp 0 < (f l).ofLp 0) (hQ : (f r).ofLp 0 < Q.ofLp 0) :

∃ (γ : ContinuousBVPaths 0 3), (∀ (s : ↑(Set.Icc 0 3)), ↑s ≤ 1 → ↑γ s = P + ↑s • (f l - P)) ∧ (∀ (s : ↑(Set.Icc 0 3)), 1 ≤ ↑s → ↑s ≤ 2 → ↑γ s = f (l + (↑s - 1) * (r - l))) ∧ (∀ (s : ↑(Set.Icc 0 3)), 2 ≤ ↑s → ↑γ s = f r + (↑s - 2) • (Q - f r)) ∧ StrictMono fun (s : ↑(Set.Icc 0 3)) => (↑γ s).ofLp 0

Three pieces — a rising segment into the left end of a strictly decreasing arc, that arc traversed backwards, and a rising segment out of its right end — assemble into a continuous BV path on [0, 3] whose first coordinate is strictly increasing.

source

theorem MovingSofa.le_of_threePieceRoof {r l α β cc : ℝ} (hrl : r < l) (f : ℝ → Point) (P Q : Point) (γ : ContinuousBVPaths 0 3) (hγ0 : ∀ (s : ↑(Set.Icc 0 3)), ↑s ≤ 1 → ↑γ s = P + ↑s • (f l - P)) (hγ1 : ∀ (s : ↑(Set.Icc 0 3)), 1 ≤ ↑s → ↑s ≤ 2 → ↑γ s = f (l + (↑s - 1) * (r - l))) (hγ2 : ∀ (s : ↑(Set.Icc 0 3)), 2 ≤ ↑s → ↑γ s = f r + (↑s - 2) • (Q - f r)) (hP : α * P.ofLp 0 + β * P.ofLp 1 ≤ cc) (hQ : α * Q.ofLp 0 + β * Q.ofLp 1 ≤ cc) (harc : ∀ t ∈ Set.Icc r l, α * (f t).ofLp 0 + β * (f t).ofLp 1 ≤ cc) (s : ↑(Set.Icc 0 3)) :

α * (↑γ s).ofLp 0 + β * (↑γ s).ofLp 1 ≤ cc

A linear functional bounded at the two base corners of a three-piece roof and along its middle arc is bounded along the whole roof.

source

theorem MovingSofa.area_region_under_strictMono_roof {r l h : ℝ} (hrl : r < l) (c : ContinuousBVPaths r l) (f : ℝ → Point) (P Q : Point) (γ : ContinuousBVPaths 0 3) (hf : ∀ (t : ℝ) (ht : t ∈ Set.Icc r l), ↑c ⟨t, ht⟩ = f t) (hP : P.ofLp 1 = -h) (hQ : Q.ofLp 1 = -h) (hγ0 : ∀ (s : ↑(Set.Icc 0 3)), ↑s ≤ 1 → ↑γ s = P + ↑s • (f l - P)) (hγ1 : ∀ (s : ↑(Set.Icc 0 3)), 1 ≤ ↑s → ↑s ≤ 2 → ↑γ s = f (l + (↑s - 1) * (r - l))) (hγ2 : ∀ (s : ↑(Set.Icc 0 3)), 2 ≤ ↑s → ↑γ s = f r + (↑s - 2) • (Q - f r)) (hγmono : StrictMono fun (s : ↑(Set.Icc 0 3)) => (↑γ s).ofLp 0) (hγlow : ∀ (s : ↑(Set.Icc 0 3)), -h ≤ (↑γ s).ofLp 1) :

ClassicalResults.area {p : Point | ∃ (s : ↑(Set.Icc 0 3)), p.ofLp 0 = (↑γ s).ofLp 0 ∧ -h ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ (↑γ s).ofLp 1} = segmentArea Q (f r) + curveAreaFunctional c + segmentArea (f l) P + segmentArea P Q

The closed region under a strictly monotone three-piece roof whose two side segments begin and end on the line y = -h has area equal to the signed area of the four-piece loop that bounds it: the base segment, the two side segments and the arc.

source

theorem MovingSofa.area_region_under_roof_le {h : ℝ} (γ : ContinuousBVPaths 0 3) (hγmono : StrictMono fun (s : ↑(Set.Icc 0 3)) => (↑γ s).ofLp 0) (R T : Set Point) (hRfin : MeasureTheory.volume R ≠ ⊤) (hTfin : MeasureTheory.volume T ≠ ⊤) (hbase : ∀ (p : Point), (∃ (s : ↑(Set.Icc 0 3)), p.ofLp 0 = (↑γ s).ofLp 0) → p.ofLp 1 = -h → p ∈ R) (hincl : {p : Point | ∃ (s : ↑(Set.Icc 0 3)), p.ofLp 0 = (↑γ s).ofLp 0 ∧ -h < p.ofLp 1 ∧ p.ofLp 1 < (↑γ s).ofLp 1} \ R ⊆ T) :

ClassicalResults.area {p : Point | ∃ (s : ↑(Set.Icc 0 3)), p.ofLp 0 = (↑γ s).ofLp 0 ∧ -h ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ (↑γ s).ofLp 1} ≤ ClassicalResults.area R + ClassicalResults.area T

Comparing the closed region under a strictly monotone roof with a base set that absorbs the region's bottom edge and a set that absorbs the rest of the open region: the roof itself is a null set, so the three areas satisfy the expected inequality.

Convex.Foundations.Development001.

Convex.BoundaryVariation.
Convex.BoundaryApproximation.
Convex.Combination.
Convex.AreaSuperlevel.
Convex.CombinationPullback.
Convex.ContactFanArea.
Convex.ExposedFaces.
Convex.Limits.
Convex.SupportEmbedding.
Convex.CombinationProperties.
Convex.EnvelopeFace.
Convex.Space.

Convex / Boundary Variation #

source

theorem MovingSofa.boundedVariationOn_of_mem_exposedEdge (K : ConvexBody Point) (f : ℝ → Point) (hf : ∀ (t : ℝ), f t ∈ exposedEdge K ↑t) (a b : ℝ) :

BoundedVariationOn f (Set.Icc a b)

Every selection of points from the exposed edges has bounded variation on bounded intervals.

Convex / Boundary Approximation #

source

theorem MovingSofa.positiveVertex_boundedVariation (K : ConvexBody Point) (a b : ℝ) (hab : a ≤ b) :

BoundedVariationOn (fun (t : ℝ) => (edgeVertices K ↑t).1) (Set.Icc a b)

source

theorem MovingSofa.exists_facePreserving_polygonApproximation (K : ConvexBody Point) (F : Finset Real.Angle) :

∃ (V : ℕ → Finset Point) (P : ℕ → ConvexBody Point), (∀ (n : ℕ), (V n).Nonempty ∧ ↑(P n) = (convexHull ℝ) ↑(V n) ∧ ↑(P n) ⊆ ↑K ∧ ∀ t ∈ F, exposedEdge (P n) t = exposedEdge K t) ∧ ∀ (n : ℕ), 1 ≤ n → Metric.hausdorffDist ↑(P n) ↑K ≤ 1 / ↑n

Convex / Combination #

source

def MovingSofa.IsConvexDomain {α : Type u} (c : ↑unitInterval → α → α → α) :

Prop

A barycentric operation has an injective realization as convex combinations in a real space.

Equations

MovingSofa.IsConvexDomain c = ∃ (V : ModuleCat ℝ) (e : α → ↑V), Function.Injective e ∧ Convex ℝ (Set.range e) ∧ ∀ (t : ↑unitInterval) (x y : α), e (c t x y) = (1 - ↑t) • e x + ↑t • e y

Instances For

source

def MovingSofa.IsConvexLinear {α : Type u} {β : Type v} (cα : ↑unitInterval → α → α → α) (cβ : ↑unitInterval → β → β → β) (f : α → β) :

Prop

Preservation of the specified barycentric operations.

Equations

MovingSofa.IsConvexLinear cα cβ f = ∀ (t : ↑unitInterval) (x y : α), f (cα t x y) = cβ t (f x) (f y)

Instances For

source

def MovingSofa.IsConvexBilinear {α : Type u} {β : Type v} {γ : Type w} (cα : ↑unitInterval → α → α → α) (cβ : ↑unitInterval → β → β → β) (cγ : ↑unitInterval → γ → γ → γ) (g : α → β → γ) :

Prop

Separate preservation of barycentric combinations in both variables.

Equations

MovingSofa.IsConvexBilinear cα cβ cγ g = ((∀ (x : α), MovingSofa.IsConvexLinear cβ cγ (g x)) ∧ ∀ (y : β), MovingSofa.IsConvexLinear cα cγ fun (x : α) => g x y)

Instances For

source

def MovingSofa.realCombination (t : ↑unitInterval) (x y : ℝ) :

ℝ

The usual barycentric combination of real numbers.

Equations

MovingSofa.realCombination t x y = (1 - ↑t) * x + ↑t * y

Instances For

source

def MovingSofa.IsQuadraticFunctional {α : Type u} (c : ↑unitInterval → α → α → α) (f : α → ℝ) :

Prop

A quadratic functional is the diagonal of a separately convex-linear real map.

Equations

MovingSofa.IsQuadraticFunctional c f = ∃ (g : α → α → ℝ), MovingSofa.IsConvexBilinear c c MovingSofa.realCombination g ∧ ∀ (x : α), f x = g x x

Instances For

source

def MovingSofa.IsConvexFunctional {α : Type u} (c : ↑unitInterval → α → α → α) (f : α → ℝ) (concave : Bool) :

Prop

Concavity or convexity according to the direction of the barycentric inequality.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def MovingSofa.segmentFunctional {α : Type u} (c : ↑unitInterval → α → α → α) (f : α → ℝ) (x y : α) (t : ℝ) :

ℝ

The segment function, extended by zero outside its parameter interval.

Equations

MovingSofa.segmentFunctional c f x y t = if ht : t ∈ Set.Icc 0 1 then f (c ⟨t, ht⟩ x y) else 0

Instances For

source

noncomputable def MovingSofa.convexDirectionalDerivative {α : Type u} (c : ↑unitInterval → α → α → α) (f : α → ℝ) (x y : α) :

ℝ

The right derivative along the barycentric segment; used for quadratic functionals.

Equations

MovingSofa.convexDirectionalDerivative c f x y = derivWithin (MovingSofa.segmentFunctional c f x y) (Set.Icc 0 1) 0

Instances For

source

def MovingSofa.convexBodyCombination (t : ↑unitInterval) (K L : ConvexBody Point) :

ConvexBody Point

Minkowski interpolation of nonempty compact convex bodies, including both endpoints.

Equations

MovingSofa.convexBodyCombination t K L = (1 - ↑t) • K + ↑t • L

Instances For

Convex / Area Superlevel #

source

theorem MovingSofa.convexBody_area_superlevel (K L : ConvexBody Point) (hK : 11 / 5 ≤ ClassicalResults.area ↑K) (hL : 11 / 5 ≤ ClassicalResults.area ↑L) (t : ↑unitInterval) :

11 / 5 ≤ ClassicalResults.area ↑(convexBodyCombination t K L)

Pulling barycentric functionals back along convex-linear maps #

A convex-linear map transports one barycentric operation to another, so every notion defined from that operation pulls back along it: a quadratic functional stays quadratic, and its directional derivative along a segment is the directional derivative between the images of the two endpoints. Neither statement needs any topology or differentiability: the two segment functions are literally equal.

source

theorem MovingSofa.IsQuadraticFunctional.comp_isConvexLinear {α : Type u} {β : Type v} {cα : ↑unitInterval → α → α → α} {cβ : ↑unitInterval → β → β → β} {F : α → β} (hF : IsConvexLinear cα cβ F) {f : β → ℝ} (hf : IsQuadraticFunctional cβ f) :

IsQuadraticFunctional cα fun (x : α) => f (F x)

A quadratic functional pulled back along a convex-linear map is quadratic.

source

theorem MovingSofa.convexDirectionalDerivative_comp_isConvexLinear {α : Type u} {β : Type v} {cα : ↑unitInterval → α → α → α} {cβ : ↑unitInterval → β → β → β} {F : α → β} (hF : IsConvexLinear cα cβ F) (f : β → ℝ) (x y : α) :

convexDirectionalDerivative cα (fun (z : α) => f (F z)) x y = convexDirectionalDerivative cβ f (F x) (F y)

The directional derivative of a functional pulled back along a convex-linear map is the directional derivative of the functional between the images.

source

theorem MovingSofa.IsConvexFunctional.comp_isConvexLinear {α : Type u} {β : Type v} {cα : ↑unitInterval → α → α → α} {cβ : ↑unitInterval → β → β → β} {F : α → β} (hF : IsConvexLinear cα cβ F) {f : β → ℝ} {concave : Bool} (hf : IsConvexFunctional cβ f concave) :

IsConvexFunctional cα (fun (x : α) => f (F x)) concave

A convex or concave functional pulled back along a convex-linear map keeps its direction of convexity.

Area lower bound from ordered support contacts #

A compact convex set K of the plane that contains a base point L = (ℓ, 0) and lies in the closed quadrant {(a, b) | ℓ ≤ a, 0 ≤ b} has area at least the shoelace expression of any finite fan L, P₀, …, P_n of support contacts taken at strictly increasing normal angles in [0, π).

Two ordered contacts span a nonnegatively oriented determinant over L: expanding the support inequalities in coordinates turns sin (β - α) · (P - L) × (Q - L) into a sum of two products of nonnegative factors. The fan triangles convexHull ℝ {L, Pᵢ, Pᵢ₊₁} therefore lie in K with area one half of their determinant, and two of them can meet only along the line through L and the contact they share, which is planar null. Finite additivity of the volume off that null set and monotonicity give the bound. Repeated contacts, zero contact vectors and collinear consecutive rays are allowed: a degenerate triangle simply has vanishing area.

source

theorem MovingSofa.planeCrossProduct_sub_nonneg_of_support {K : Set Point} {L P Q : Point} (hL : L ∈ K) (hquadrant : ∀ p ∈ K, L.ofLp 0 ≤ p.ofLp 0 ∧ 0 ≤ p.ofLp 1) {α β : ℝ} (hα : 0 ≤ α) (hαβ : α < β) (hβ : β < Real.pi) (hP : P ∈ K) (hQ : Q ∈ K) (hPs : ∀ x ∈ K, inner ℝ x (normalVector ↑α) ≤ inner ℝ P (normalVector ↑α)) (hQs : ∀ x ∈ K, inner ℝ x (normalVector ↑β) ≤ inner ℝ Q (normalVector ↑β)) :

0 ≤ planeCrossProduct (P - L) (Q - L)

Two ordered support contacts of a set lying in the closed quadrant above a base point have nonnegative oriented determinant over that base point.

source

theorem MovingSofa.supportContact_fan_area (K : Set Point) (hcK : IsCompact K) (hvK : Convex ℝ K) (L : Point) (hL : L ∈ K) (hLy : L.ofLp 1 = 0) (hquadrant : ∀ p ∈ K, L.ofLp 0 ≤ p.ofLp 0 ∧ 0 ≤ p.ofLp 1) (n : ℕ) (θ : Fin (n + 1) → ℝ) (hθ : StrictMono θ) (hθrange : ∀ (i : Fin (n + 1)), 0 ≤ θ i ∧ θ i < Real.pi) (P : Fin (n + 1) → Point) (hP : ∀ (i : Fin (n + 1)), P i ∈ K) (hsupport : ∀ (i : Fin (n + 1)), ∀ q ∈ K, inner ℝ q (normalVector ↑(θ i)) ≤ inner ℝ (P i) (normalVector ↑(θ i))) :

0 ≤ 1 / 2 * ∑ i : Fin n, planeCrossProduct (P i.castSucc - L) (P i.succ - L) ∧ 1 / 2 * ∑ i : Fin n, planeCrossProduct (P i.castSucc - L) (P i.succ - L) ≤ ClassicalResults.area K

Convex / Exposed Faces #

source

theorem MovingSofa.exposedEdge_convexBodyCombination (K L : ConvexBody Point) (a : Real.Angle) (t : ↑unitInterval) :

exposedEdge (convexBodyCombination t K L) a = (1 - ↑t) • exposedEdge K a + ↑t • exposedEdge L a

Exposed faces commute with convex interpolation, including zero and unit weights.

Convex / Limits #

source

noncomputable def MovingSofa.vectorSupport (S : Set Point) (u : Point) :

ℝ

The supremum of scalar products with a specified direction vector.

Equations

MovingSofa.vectorSupport S u = sSup ((fun (x : MovingSofa.Point) => inner ℝ x u) '' S)

Instances For

source

theorem MovingSofa.abs_vectorSupport_sub_le_hausdorffDist {S T : Set Point} (hS : S.Nonempty) (hcS : IsCompact S) (hT : T.Nonempty) (hcT : IsCompact T) {u : Point} (hu : ‖u‖ = 1) :

|vectorSupport S u - vectorSupport T u| ≤ Metric.hausdorffDist S T

Support values in a unit direction vary by at most the Hausdorff distance.

source

theorem MovingSofa.convexBody_selection (A : Set Point) (hA : IsCompact A) (K : ℕ → ConvexBody Point) (hK : ∀ (n : ℕ), ↑(K n) ⊆ A) :

∃ (φ : ℕ → ℕ) (L : ConvexBody Point), StrictMono φ ∧ Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K (φ n)) ↑L) Filter.atTop (nhds 0)

source

theorem MovingSofa.compactSet_support_continuity (S T : Set Point) (hS : S.Nonempty) (hcS : IsCompact S) (hT : T.Nonempty) (hcT : IsCompact T) :

(∀ (u v : Point), ‖u‖ = 1 → ‖v‖ = 1 → |vectorSupport S u - vectorSupport S v| ≤ sSup (norm '' S) * ‖u - v‖) ∧ (∀ (u : Point), ‖u‖ = 1 → |vectorSupport S u - vectorSupport T u| ≤ Metric.hausdorffDist S T) ∧ (Continuous fun (t : Real.Angle) => supportValue S t) ∧ ∀ (K : ℕ → Set Point), (∀ (n : ℕ), (K n).Nonempty ∧ IsCompact (K n)) → Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist (K n) S) Filter.atTop (nhds 0) → TendstoUniformlyOn (fun (n : ℕ) (u : Point) => vectorSupport (K n) u) (vectorSupport S) Filter.atTop {u : Point | ‖u‖ = 1}

source

theorem MovingSofa.fixedNormalBody_closed (U : Set Point) (hU : ∀ u ∈ U, ‖u‖ = 1) (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hK : ∀ (n : ℕ), ↑(K n) = ⋂ u ∈ U, {x : Point | inner ℝ x u ≤ vectorSupport (↑(K n)) u}) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) :

↑L = ⋂ u ∈ U, {x : Point | inner ℝ x u ≤ vectorSupport (↑L) u}

source

theorem MovingSofa.convexArea_hausdorff_continuity (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) :

Filter.Tendsto (fun (n : ℕ) => ClassicalResults.area ↑(K n)) Filter.atTop (nhds (ClassicalResults.area ↑L))

source

theorem MovingSofa.continuous_supportValue (K : ConvexBody Point) :

Continuous fun (t : Real.Angle) => supportValue (↑K) t

The support function of a convex body is continuous in the normal direction.

source

theorem MovingSofa.continuous_supportValue_real (K : ConvexBody Point) :

Continuous fun (t : ℝ) => supportValue ↑K ↑t

source

theorem MovingSofa.abs_supportValue_sub_le_of_isCompact {s : Set Point} (hne : s.Nonempty) (hc : IsCompact s) (x y : ℝ) :

|supportValue s ↑x - supportValue s ↑y| ≤ sSup (norm '' s) * |x - y|

Support values of a nonempty compact set are Lipschitz in the real angle, with the largest norm of a point of the set as Lipschitz constant.

Convex / Support Embedding #

source

theorem MovingSofa.supportFunction_minkowski_embedding (K L : ConvexBody Point) :

(∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → ∀ (t : Real.Angle), supportValue {z : Point | ∃ x ∈ ↑K, ∃ y ∈ ↑L, z = a • x + b • y} t = a * supportValue (↑K) t + b * supportValue (↑L) t) ∧ ((∀ (t : Real.Angle), supportValue (↑K) t = supportValue (↑L) t) → K = L) ∧ (Continuous fun (t : Real.Angle) => supportValue (↑K) t) ∧ ↑K = ⋂ u ∈ {u : Point | ‖u‖ = 1}, {p : Point | inner ℝ p u ≤ vectorSupport (↑K) u}

Convex / Combination Properties #

source

theorem MovingSofa.mem_convexBodyCombination_iff (t : ↑unitInterval) (K L : ConvexBody Point) (z : Point) :

z ∈ ↑(convexBodyCombination t K L) ↔ ∃ x ∈ ↑K, ∃ y ∈ ↑L, z = (1 - ↑t) • x + ↑t • y

Pointwise description of the Minkowski interpolation of two convex bodies.

source

theorem MovingSofa.inner_le_edgeVertices_fst_tangent (K : ConvexBody Point) (a : Real.Angle) {p : Point} (hp : p ∈ exposedEdge K a) :

inner ℝ p (tangentVector a) ≤ inner ℝ (edgeVertices K a).1 (tangentVector a)

The first edge vertex maximizes tangent coordinate on its exposed edge.

source

theorem MovingSofa.edgeVertices_fst_eq_of_tangent_isGreatest (K : ConvexBody Point) (a : Real.Angle) {p : Point} (hp : p ∈ exposedEdge K a) (hmax : ∀ q ∈ exposedEdge K a, inner ℝ q (tangentVector a) ≤ inner ℝ p (tangentVector a)) :

(edgeVertices K a).1 = p

A tangent-coordinate maximizer on an exposed edge is its first vertex.

source

theorem MovingSofa.edgeVertices_snd_eq_of_tangent_isLeast (K : ConvexBody Point) (a : Real.Angle) {p : Point} (hp : p ∈ exposedEdge K a) (hmin : ∀ q ∈ exposedEdge K a, inner ℝ p (tangentVector a) ≤ inner ℝ q (tangentVector a)) :

(edgeVertices K a).2 = p

A tangent-coordinate minimizer on an exposed edge is its second vertex.

source

theorem MovingSofa.edgeVertices_convexBodyCombination (t : ↑unitInterval) (K L : ConvexBody Point) (a : Real.Angle) :

(edgeVertices (convexBodyCombination t K L) a).1 = (1 - ↑t) • (edgeVertices K a).1 + ↑t • (edgeVertices L a).1 ∧ (edgeVertices (convexBodyCombination t K L) a).2 = (1 - ↑t) • (edgeVertices K a).2 + ↑t • (edgeVertices L a).2

The extreme points of exposed edges commute with convex combinations.

source

theorem MovingSofa.supportValue_convexBodyCombination (t : ↑unitInterval) (K L : ConvexBody Point) (a : Real.Angle) :

supportValue (↑(convexBodyCombination t K L)) a = (1 - ↑t) * supportValue (↑K) a + ↑t * supportValue (↑L) a

Support values commute with convex combinations.

Faces of a body cut out by a differentiable family of half-planes #

Let L be a convex body lying in every half-plane {q | m s ≤ ⟪q, u_s⟫} of a family indexed by a real angle parameter s, and let p ∈ L attain the bound at s = t. If m is differentiable at t with m' t = ⟪p, v_t⟫ — that is, if p is the first-order contact point of the family — then the reversed face of L at t + π is pinned down by the sign of the one-sided derivatives of s ↦ ⟪z, u_s⟫ - m s at t: exposedEdge_add_pi_eq_singleton_of_mem_Ioo at an interior parameter gives the singleton {p}, while edgeVertices_add_pi_fst_eq_of_lt and edgeVertices_add_pi_snd_eq_of_lt identify p with one endpoint vertex of the face at the two boundary parameters.

source

theorem MovingSofa.inner_tangentVector_le_of_forall_le_Ioo {m : ℝ → ℝ} {p z : Point} {a t : ℝ} (hat : a < t) (hle : ∀ s ∈ Set.Ioo a t, m s ≤ inner ℝ z (normalVector ↑s)) (hzm : inner ℝ z (normalVector ↑t) = m t) (hd : HasDerivAt m (inner ℝ p (tangentVector ↑t)) t) :

inner ℝ z (tangentVector ↑t) ≤ inner ℝ p (tangentVector ↑t)

The tangent coordinate of a point whose normal coordinate dominates a differentiable family to the left of the touching parameter is at most that of the contact point.

source

theorem MovingSofa.le_inner_tangentVector_of_forall_le_Ioo {m : ℝ → ℝ} {p z : Point} {t b : ℝ} (htb : t < b) (hle : ∀ s ∈ Set.Ioo t b, m s ≤ inner ℝ z (normalVector ↑s)) (hzm : inner ℝ z (normalVector ↑t) = m t) (hd : HasDerivAt m (inner ℝ p (tangentVector ↑t)) t) :

inner ℝ p (tangentVector ↑t) ≤ inner ℝ z (tangentVector ↑t)

The tangent coordinate of a point whose normal coordinate dominates a differentiable family to the right of the touching parameter is at least that of the contact point.

source

theorem MovingSofa.exposedEdge_add_pi_eq_singleton_of_mem_Ioo {L : ConvexBody Point} {m : ℝ → ℝ} {p : Point} {a b t : ℝ} (ht : t ∈ Set.Ioo a b) (hle : ∀ q ∈ ↑L, ∀ s ∈ Set.Ioo a b, m s ≤ inner ℝ q (normalVector ↑s)) (hp : p ∈ ↑L) (hpm : inner ℝ p (normalVector ↑t) = m t) (hd : HasDerivAt m (inner ℝ p (tangentVector ↑t)) t) :

exposedEdge L ↑(t + Real.pi) = {p}

At an interior touching parameter of a differentiable family of supporting half-planes the reversed face is the singleton contact point.

source

theorem MovingSofa.edgeVertices_add_pi_fst_eq_of_lt {L : ConvexBody Point} {m : ℝ → ℝ} {p : Point} {a b : ℝ} (hab : a < b) (hle : ∀ q ∈ ↑L, ∀ s ∈ Set.Ioo a b, m s ≤ inner ℝ q (normalVector ↑s)) (hlea : ∀ q ∈ ↑L, m a ≤ inner ℝ q (normalVector ↑a)) (hp : p ∈ ↑L) (hpm : inner ℝ p (normalVector ↑a) = m a) (hd : HasDerivAt m (inner ℝ p (tangentVector ↑a)) a) :

(edgeVertices L ↑(a + Real.pi)).1 = p

At the left endpoint parameter of a differentiable family of supporting half-planes the contact point is the positive vertex of the reversed face.

source

theorem MovingSofa.edgeVertices_add_pi_snd_eq_of_lt {L : ConvexBody Point} {m : ℝ → ℝ} {p : Point} {a b : ℝ} (hab : a < b) (hle : ∀ q ∈ ↑L, ∀ s ∈ Set.Ioo a b, m s ≤ inner ℝ q (normalVector ↑s)) (hleb : ∀ q ∈ ↑L, m b ≤ inner ℝ q (normalVector ↑b)) (hp : p ∈ ↑L) (hpm : inner ℝ p (normalVector ↑b) = m b) (hd : HasDerivAt m (inner ℝ p (tangentVector ↑b)) b) :

(edgeVertices L ↑(b + Real.pi)).2 = p

At the right endpoint parameter of a differentiable family of supporting half-planes the contact point is the negative vertex of the reversed face.

Convex / Space #

source

theorem MovingSofa.convexBody_isConvexDomain :

IsConvexDomain convexBodyCombination

Convex bodies form a convex domain under Minkowski interpolation.

Area.Foundations.Development001.

Area.ModuloLinear.
Area.Quadratic.

Area / Modulo Linear #

source

def MovingSofa.EquivalentModuloConvexLinear {α : Type u} (c : ↑unitInterval → α → α → α) (f g : α → ℝ) :

Prop

The difference of two functionals preserves the specified convex combinations.

Equations

MovingSofa.EquivalentModuloConvexLinear c f g = MovingSofa.IsConvexLinear c MovingSofa.realCombination fun (x : α) => f x - g x

Instances For

Area / Quadratic #

source

theorem MovingSofa.convexDirectionalDerivative_eq_of_hasDerivWithinAt {α : Type u} (c : ↑unitInterval → α → α → α) (f : α → ℝ) (x y : α) {d : ℝ} (h : HasDerivWithinAt (segmentFunctional c f x y) d (Set.Icc 0 1) 0) :

convexDirectionalDerivative c f x y = d

The directional derivative along a barycentric segment is computed by any derivative of the segment function at the base point.

source

theorem MovingSofa.quadratic_directional_derivative {α : Type u} (c : ↑unitInterval → α → α → α) (f : α → ℝ) (h : α → α → ℝ) (hh : IsConvexBilinear c c realCombination h) (hf : ∀ (x : α), f x = h x x) :

(∀ (x y : α), HasDerivWithinAt (segmentFunctional c f x y) (h x y + h y x - 2 * h x x) (Set.Icc 0 1) 0) ∧ (∀ (x y : α), convexDirectionalDerivative c f x y = h x y + h y x - 2 * h x x) ∧ ∀ (x : α), IsConvexLinear c realCombination fun (y : α) => convexDirectionalDerivative c f x y

A quadratic diagonal has the stated segment derivative, affine in its destination.

source

theorem MovingSofa.IsQuadraticFunctional.hasDerivWithinAt_segmentFunctional {α : Type u} {c : ↑unitInterval → α → α → α} {f : α → ℝ} (hf : IsQuadraticFunctional c f) (x y : α) :

HasDerivWithinAt (segmentFunctional c f x y) (convexDirectionalDerivative c f x y) (Set.Icc 0 1) 0

The segment function of a quadratic functional is differentiable at the base point, with the directional derivative as its derivative.

source

theorem MovingSofa.quadratic_maximum_iff {α : Type u} (c : ↑unitInterval → α → α → α) (hc : IsConvexDomain c) (f : α → ℝ) (hq : IsQuadraticFunctional c f) (hconcave : IsConvexFunctional c f true) (x : α) :

(∀ (y : α), f y ≤ f x) ↔ ∀ (y : α), convexDirectionalDerivative c f x y ≤ 0

A concave quadratic functional is maximized exactly where all directional derivatives are nonpositive.

source

theorem MovingSofa.IsQuadraticFunctional.add {α : Type u} {c : ↑unitInterval → α → α → α} {f g : α → ℝ} (hf : IsQuadraticFunctional c f) (hg : IsQuadraticFunctional c g) :

IsQuadraticFunctional c fun (x : α) => f x + g x

A sum of quadratic functionals is quadratic.

source

theorem MovingSofa.IsConvexFunctional.add {α : Type u} {c : ↑unitInterval → α → α → α} {f g : α → ℝ} {concave : Bool} (hf : IsConvexFunctional c f concave) (hg : IsConvexFunctional c g concave) :

IsConvexFunctional c (fun (x : α) => f x + g x) concave

A sum of convex functionals is convex, and a sum of concave functionals is concave.

source

theorem MovingSofa.IsConvexLinear.isConvexFunctional {α : Type u} {c : ↑unitInterval → α → α → α} {f : α → ℝ} (hf : IsConvexLinear c realCombination f) (concave : Bool) :

IsConvexFunctional c f concave

A convex-linear real functional satisfies both barycentric inequalities, with equality.

source

theorem MovingSofa.IsConvexLinear.isQuadraticFunctional {α : Type u} {c : ↑unitInterval → α → α → α} {f : α → ℝ} (hf : IsConvexLinear c realCombination f) :

IsQuadraticFunctional c f

A convex-linear real functional is quadratic: it is the diagonal of the mean of its values.

source

theorem MovingSofa.IsConvexFunctional.neg {α : Type u} {c : ↑unitInterval → α → α → α} {f : α → ℝ} {concave : Bool} (hf : IsConvexFunctional c f concave) :

IsConvexFunctional c (fun (x : α) => -f x) !concave

Negation exchanges convexity and concavity.

source

theorem MovingSofa.IsQuadraticFunctional.neg {α : Type u} {c : ↑unitInterval → α → α → α} {f : α → ℝ} (hf : IsQuadraticFunctional c f) :

IsQuadraticFunctional c fun (x : α) => -f x

The negative of a quadratic functional is quadratic.

Geometry.Foundations.Development002.

Geometry.Convex.FrontierInterior.
Geometry.RadialBoundary.

Geometry / Convex / Frontier Interior #

source

theorem MovingSofa.connectedComponentIn_compl_frontier_subset_interior {s : Set Point} (hs : IsClosed s) {p : Point} (hp : p ∈ interior s) :

connectedComponentIn (frontier s)ᶜ p ⊆ interior s

A bounded component of the frontier complement that meets the set lies in its interior.

source

theorem MovingSofa.interior_subset_jordanInterior_frontier {s : Set Point} (hs : IsClosed s) (hb : Bornology.IsBounded s) :

interior s ⊆ jordanInterior (frontier s)

The interior of a bounded closed set lies in the bounded component of its frontier complement.

source

theorem MovingSofa.ray_smul_sub_notMem {s : Set Point} (hs : Convex ℝ s) {o p : Point} (ho : o ∈ s) (hp : p ∉ s) {r : ℝ} (hr : 1 ≤ r) :

o + r • (p - o) ∉ s

The outward ray from a point outside a convex set remains outside the set.

source

theorem MovingSofa.exterior_component_unbounded {s : Set Point} (hs : Convex ℝ s) (hclosed : IsClosed s) {o p : Point} (ho : o ∈ s) (hp : p ∉ s) :

¬Bornology.IsBounded (connectedComponentIn (frontier s)ᶜ p)

Every exterior point of a nonempty bounded closed convex set has an unbounded component outside its frontier.

source

theorem MovingSofa.jordanInterior_frontier_eq_interior {s : Set Point} (hs : Convex ℝ s) (hclosed : IsClosed s) (hb : Bornology.IsBounded s) (hne : s.Nonempty) :

jordanInterior (frontier s) = interior s

The bounded complementary region of a nonempty compact convex set frontier is its interior.

Geometry / Radial Boundary #

source

theorem MovingSofa.convexBody_radial_boundary (K : ConvexBody Point) (o : Point) (ho : o ∈ interior ↑K) :

∃ (ρ : Point → ℝ) (e : ↑{u : Point | ‖u‖ = 1} ≃ₜ ↑(frontier ↑K)) (C : NNReal) (γ : ContinuousBVPaths 0 (2 * Real.pi)), (∀ (u : Point), ‖u‖ = 1 → 0 < ρ u ∧ o + ρ u • u ∈ frontier ↑K ∧ ∀ (r : ℝ), 0 < r → o + r • u ∈ frontier ↑K → r = ρ u) ∧ (∀ (u : ↑{u : Point | ‖u‖ = 1}), ↑(e u) = o + ρ ↑u • ↑u) ∧ (LipschitzWith C fun (u : ↑{u : Point | ‖u‖ = 1}) => ↑(e u)) ∧ (∀ (t : ↑(Set.Icc 0 (2 * Real.pi))), ↑γ t = o + ρ (normalVector ↑↑t) • normalVector ↑↑t) ∧ IsOrientedJordanParametrization curveWinding_radial_center._proof_1 (frontier ↑K) true ↑γ ∧ jordanInterior (frontier ↑K) = interior ↑K

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Analysis / Bounded Variation #

Analysis / Measure Products #

The oriented planar determinant #

Analysis / Stieltjes / Integral #

Analysis / Stieltjes / Absolute Continuity #

Analysis / Stieltjes / Calculus #

Analysis / Stieltjes / Density Integration #

Analysis / Stieltjes / Linearity #

Analysis / Stieltjes / Inner Product #

Analysis / Stieltjes / Smooth #

Analysis / Stieltjes / Frame #

Analysis / Stieltjes / Transport #

Analysis / Stieltjes / Continuous #

Analysis / Stieltjes / Affine #

Riemann-Stieltjes sums for continuous integrands #

Analysis / Stieltjes / Shift #

Analysis / Surface Measure / Basic #

Analysis / Surface Measure / Exterior Normal #

Analysis / Surface Measure / Graph Definitions #

Analysis / Surface Measure / Regularity #

Analysis / Surface Measure / Segment #

Analysis / Surface Measure / Segment Faces #

Analysis / Surface Measure / Segment Graph #

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Curve / Area #

Curve / Area Transport #

Curve / Concatenation #

Curve / Area Additivity #

Curve / Cyclic Rotation #

Curve / Jordan / Basic #

Curve / Jordan / Orientation #

Curve / Jordan / Area #

Curve / Jordan / Arc Area #

Curve / Jordan / Parametrization #

Curve / Jordan / Unit Sphere #

Curve / Jordan / Winding #

Curve / Jordan / Radial Winding #

Curve / Jordan / Winding Concatenation #

Curve / Jordan / Cyclic Rotation #

Curve / Jordan / Winding Kernel #

Curve / Jordan / Winding Local Constancy #

Curve / Jordan / Winding Lifts #

The range of an almost injective continuous BV path is null #

Curve / Segment Area #

Curve / Segment Area / Parametrization #

Curve / Smooth Interval Paths #

Curve / Jordan / Radial Loop #

A Stieltjes chain rule with a local quadratic remainder #

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Area / Monotone Roof #

Three-piece monotone roofs #

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Convex / Boundary Variation #

Convex / Boundary Approximation #

Convex / Combination #

Convex / Area Superlevel #

Pulling barycentric functionals back along convex-linear maps #

Area lower bound from ordered support contacts #

Convex / Exposed Faces #

Convex / Limits #

Convex / Support Embedding #

Convex / Combination Properties #

Faces of a body cut out by a differentiable family of half-planes #

Convex / Space #

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Area / Modulo Linear #

Area / Quadratic #

Moving sofa: related mathematical developments #

Moving sofa: related mathematical developments #

Geometry / Convex / Frontier Interior #

Geometry / Radial Boundary #