Documentation

theorem MovingSofa.exists_density_le_of_domination {a b : ℝ} (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hμ : μ (Set.Icc a b)ᶜ = 0) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Icc a b))) (hf_nonneg : ∀ t ∈ Set.Icc a b, 0 ≤ f t) {M : ℝ} (hf_bound : ∀ t ∈ Set.Icc a b, f t ≤ M) (hdom : ∀ (E : Set ℝ), MeasurableSet E → E ⊆ Set.Icc a b → μ E ≤ ENNReal.ofReal (∫ (t : ℝ) in E, f t)) :

∃ (r : ℝ → ℝ), Measurable r ∧ MeasureTheory.IntegrableOn r (Set.Icc a b) MeasureTheory.volume ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), 0 ≤ r t ∧ r t ≤ f t) ∧ μ = (MeasureTheory.volume.restrict (Set.Icc a b)).withDensity fun (t : ℝ) => ENNReal.ofReal (r t)

A finite measure carried by Set.Icc a b and dominated on that interval by the integral of a bounded, almost everywhere strongly measurable nonnegative function f has an integrable real density with respect to the Lebesgue measure on Set.Icc a b, and that density is bounded above by f almost everywhere.

theorem MovingSofa.exists_nnreal_density_of_domination {a b : ℝ} (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (hμ : μ (Set.Icc a b)ᶜ = 0) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Icc a b))) (hf_nonneg : ∀ t ∈ Set.Icc a b, 0 ≤ f t) {M : ℝ} (hf_bound : ∀ t ∈ Set.Icc a b, f t ≤ M) (hdom : ∀ (E : Set ℝ), MeasurableSet E → E ⊆ Set.Icc a b → μ E ≤ ENNReal.ofReal (∫ (t : ℝ) in E, f t)) :

∃ (r : ℝ → NNReal), Measurable r ∧ μ = (MeasureTheory.volume.restrict (Set.Icc a b)).withDensity fun (t : ℝ) => ↑(r t)

A finite measure carried by Set.Icc a b and dominated on that interval by the integral of a bounded, almost everywhere strongly measurable nonnegative function has a measurable ℝ≥0-valued density with respect to the Lebesgue measure on Set.Icc a b.

Classical.Foundations.Development001.

Classical.Area.

Planar area #

The real-valued Lebesgue area of a planar set, and its invariance under translation.

@[reducible, inline]

abbrev MovingSofa.ClassicalResults.Plane :

The Euclidean plane.

Equations

MovingSofa.ClassicalResults.Plane = EuclideanSpace ℝ (Fin 2)

Instances For

noncomputable def MovingSofa.ClassicalResults.area (s : Set Plane) :

The real-valued Lebesgue area of a planar set.

Equations

MovingSofa.ClassicalResults.area s = (MeasureTheory.volume s).toReal

Instances For

theorem MovingSofa.ClassicalResults.area_image_add (S : Set Plane) (v : Plane) :

area ((fun (p : Plane) => p + v) '' S) = area S

Planar area is invariant under translation.

ForMathlib.Algebra.Foundations.Development001.
ForMathlib.Analysis.Foundations.Development001.
ForMathlib.BoundedVariation.Foundations.Development001.
ForMathlib.Convex.Foundations.Development001.
ForMathlib.Geometry.Foundations.Development001.
ForMathlib.MeasureTheory.Foundations.Development001.
ForMathlib.Order.Foundations.Development001.
ForMathlib.Topology.Foundations.Development001.
ForMathlib.MeasureTheory.Foundations.Development002.

ForMathlib.Algebra.BigOperators.Triangle.
ForMathlib.Algebra.Order.Fin.

Triangular rearrangement of a double sum over a `Finset` #

A double sum over s ×ˢ s splits into the closed lower triangle {(u, t) | u ≤ t} and its transpose. The two pieces overlap exactly on the diagonal, so for a kernel vanishing there the lower-triangular sum plus its transpose recovers the whole double sum.

Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag is the Fintype and LocallyFiniteOrder analogue, and Fin.sum_sum_eq_sum_triangle_add the Fin analogue; neither applies to a general Finset of a plain LinearOrder.

theorem Finset.sum_filter_le_add_sum_filter_le_swap {ι : Type u_1} {M : Type u_2} [LinearOrder ι] [AddCommMonoid M] (s : Finset ι) (f : ι → ι → M) (hdiag : ∀ (x : ι), f x x = 0) :

∑ t ∈ s, ∑ u ∈ s with u ≤ t, f u t + ∑ t ∈ s, ∑ u ∈ s with u ≤ t, f t u = ∑ x ∈ s, ∑ y ∈ s, f x y

For a kernel vanishing on the diagonal, the closed lower-triangular double sum plus the same sum with the two arguments swapped is the full double sum.

For Mathlib / Algebra / Order / Fin #

theorem Fin.apply_le_last_add_sum_max_sub {n : ℕ} (f : Fin (n + 1) → ℝ) (i : Fin (n + 1)) :

f i ≤ f (last n) + ∑ j : Fin n, max (f j.castSucc - f j.succ) 0

A finite sequence is bounded by its final value plus its positive backward increments.

ForMathlib.Analysis.Calculus.Deriv.Shift.
ForMathlib.Analysis.Calculus.FirstReturn.
ForMathlib.Analysis.Calculus.Interval.
ForMathlib.Analysis.Calculus.LocalExtr.OneSided.
ForMathlib.Analysis.Complex.DiskIntegral.
ForMathlib.Analysis.Convex.Basic.
ForMathlib.Analysis.Convex.Deriv.
ForMathlib.Analysis.Convex.Gauge.
ForMathlib.Analysis.Convex.GaugeRescale.
ForMathlib.Analysis.Convex.Radial.
ForMathlib.Analysis.FiniteEnvelope.
ForMathlib.Analysis.InnerProductSpace.Box.
ForMathlib.Analysis.InnerProductSpace.Linear.
ForMathlib.Analysis.Normed.Affine.ContinuousAffineMap.
ForMathlib.Analysis.SpecialFunctions.Angle.
ForMathlib.Analysis.SpecialFunctions.AngleLift.
ForMathlib.Analysis.SpecialFunctions.Arctan.
ForMathlib.Analysis.SpecificLimits.AlternatingBracket.
ForMathlib.Analysis.SpecialFunctions.Trigonometric.

Shifting the base point of a derivative #

HasDerivAt.comp_add_const transports a derivative at a shifted base point to the shifted function; this file records the converse implication, packaged as an Iff.

theorem hasDerivAt_comp_add_const_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (x a : 𝕜) :

HasDerivAt (fun (u : 𝕜) => f (u + a)) f' x ↔ HasDerivAt f f' (x + a)

A derivative at a shifted base point is the derivative of the shifted function.

First return to a level #

A continuous real function that starts strictly below a level and reaches it has a smallest time at which it attains that level, and its derivative there is nonnegative.

theorem exists_first_return {g : ℝ → ℝ} {a b c : ℝ} (hab : a < b) (hcont : ContinuousOn g (Set.Icc a b)) (hga : g a < c) (hgb : c ≤ g b) :

∃ t ∈ Set.Ioc a b, g t = c ∧ ∀ u ∈ Set.Ico a t, g u < c

A continuous function below a level at the left end has a first return to that level.

theorem nonneg_of_first_return {g : ℝ → ℝ} {a t c d : ℝ} (hat : a < t) (hd : HasDerivAt g d t) (hgt : g t = c) (hleft : ∀ u ∈ Set.Ico a t, g u < c) :

0 ≤ d

At a first return from below, the derivative is nonnegative.

For Mathlib / Analysis / Calculus / Interval #

theorem hasDerivWithinAt_Icc_of_oneSided {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b t : ℝ} (hab : a < b) (ht : t ∈ Set.Icc a b) {f : ℝ → E} {d : E} (hr : t < b → HasDerivWithinAt f d (Set.Ici t) t) (hl : a < t → HasDerivWithinAt f d (Set.Iic t) t) :

HasDerivWithinAt f d (Set.Icc a b) t

Glue one-sided derivatives on a closed interval, including its endpoints.

theorem contDiffOn_one_of_continuous_derivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (f : ℝ → E) (d : ↑s → E) (hd : Continuous d) (hf : ∀ (t : ↑s), HasDerivWithinAt f (d t) s ↑t) :

ContDiffOn ℝ 1 f s

A continuous derivative field on a uniquely differentiable set gives order-one regularity.

theorem hasDerivAt_if_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g f' g' : ℝ → E} {c : ℝ} (hf : ∀ (t : ℝ), HasDerivAt f (f' t) t) (hg : ∀ (t : ℝ), HasDerivAt g (g' t) t) (hfg : f c = g c) (hfg' : f' c = g' c) (t : ℝ) :

HasDerivAt (fun (s : ℝ) => if s ≤ c then f s else g s) (if t ≤ c then f' t else g' t) t

Glue two everywhere differentiable functions along the switch {s ≤ c}. If the values and the derivatives agree at c, the glued function is differentiable everywhere and its derivative is the analogous glue of the two derivative fields. At c itself the statement is genuine two-sided differentiability, obtained from the two one-sided derivatives.

theorem contDiff_one_of_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f f' : ℝ → E} (hf : ∀ (t : ℝ), HasDerivAt f (f' t) t) (hf' : Continuous f') :

ContDiff ℝ 1 f

A globally defined continuous derivative field witnesses continuous differentiability.

Fermat's theorem for one-sided derivatives on the real line #

IsLocalMinOn.hasFDerivWithinAt_nonneg signs a derivative within a set against the positive tangent cone of that set. On the real line the positive tangent cones of the two half-lines at a are generated by 1 and by -1, which turns that statement into the two familiar one-sided derivative tests at a one-sided minimum.

theorem one_mem_posTangentConeAt_Ici (a : ℝ) :

1 ∈ posTangentConeAt (Set.Ici a) a

The forward direction belongs to the positive tangent cone of a right half-line.

theorem neg_one_mem_posTangentConeAt_Iic (a : ℝ) :

-1 ∈ posTangentConeAt (Set.Iic a) a

The backward direction belongs to the positive tangent cone of a left half-line.

theorem IsLocalMinOn.hasDerivWithinAt_Ici_nonneg {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMinOn f (Set.Ici a) a) (hf : HasDerivWithinAt f f' (Set.Ici a) a) :

0 ≤ f'

A right derivative at a minimum over a right half-line is nonnegative.

theorem IsLocalMinOn.hasDerivWithinAt_Iic_nonpos {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMinOn f (Set.Iic a) a) (hf : HasDerivWithinAt f f' (Set.Iic a) a) :

f' ≤ 0

A left derivative at a minimum over a left half-line is nonpositive.

For Mathlib / Analysis / Complex / Disk Integral #

theorem Complex.integrableOn_inv_norm_ball (S : ℝ) :

MeasureTheory.IntegrableOn (fun (p : ℂ) => ‖p‖⁻¹) (Metric.ball 0 S) MeasureTheory.volume

Inverse distance from zero is integrable on a complex disk centred at zero.

theorem Complex.setIntegral_inv_norm_ball (S : ℝ) (hS : 0 < S) :

∫ (p : ℂ) in Metric.ball 0 S, ‖p‖⁻¹ = 2 * Real.pi * S

The integral of inverse distance from zero over a complex disk centred at zero.

theorem Complex.setIntegral_inv_sub_ball (R : ℝ) (a : ℂ) (ha : ‖a‖ < R) :

∫ (q : ℂ) in Metric.ball 0 R, (a - q)⁻¹ = ↑Real.pi * (starRingEnd ℂ) a

The integral of q ↦ (a - q)⁻¹ over a disk centred at zero containing a.

For Mathlib / Analysis / Convex / Basic #

theorem Convex.smul_mem_of_nonneg_of_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) {v : E} {x a : ℝ} (hzero : 0 ∈ s) (ha : a • v ∈ s) (hx : 0 ≤ x) (hxa : x ≤ a) :

x • v ∈ s

Every nonnegative scalar between zero and a known scalar multiple stays in a convex set.

For Mathlib / Analysis / Convex / Deriv #

theorem ConcaveOn.le_add_deriv_mul_sub {s : Set ℝ} {g : ℝ → ℝ} (hg : ConcaveOn ℝ s g) {x : ℝ} (hx : x ∈ s) (hdiff : DifferentiableAt ℝ g x) {y : ℝ} (hy : y ∈ s) :

g y ≤ g x + deriv g x * (y - x)

A differentiable concave real function lies below its tangent line.

theorem ConcaveOn.tendsto_deriv_of_tendsto_Ioo {ι : Type u_1} {F : Filter ι} {f : ι → ℝ → ℝ} {g : ℝ → ℝ} {a b x : ℝ} (hx : x ∈ Set.Ioo a b) (hf : ∀ᶠ (n : ι) in F, ConcaveOn ℝ (Set.Ioo a b) (f n)) (hlim : ∀ y ∈ Set.Ioo a b, Filter.Tendsto (fun (n : ι) => f n y) F (nhds (g y))) (hdf : ∀ᶠ (n : ι) in F, DifferentiableAt ℝ (f n) x) (hdg : DifferentiableAt ℝ g x) :

Filter.Tendsto (fun (n : ι) => deriv (f n) x) F (nhds (deriv g x))

Pointwise convergence of concave functions forces derivative convergence at a common differentiability point in the interior of an interval.

For Mathlib / Analysis / Convex / Gauge #

theorem Convex.existsUnique_pos_smul_mem_frontier_of_gauge_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) {u : E} (hu : 0 < gauge s u) :

∃! r : ℝ , 0 < r ∧ r • u ∈ frontier s

A direction of positive gauge has a unique positive multiple on the frontier.

theorem Convex.existsUnique_pos_smul_mem_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) (hb : Bornology.IsVonNBounded ℝ s) {u : E} (hu : u ≠ 0) :

∃! r : ℝ , 0 < r ∧ r • u ∈ frontier s

Every nonzero direction has a unique positive multiple on the frontier of a bounded convex neighborhood of zero.

theorem Real.dist_inv_le_of_pos_lower_bound {a b c : ℝ} (hc : 0 < c) (ha : c ≤ a) (hb : c ≤ b) :

dist a⁻¹ b⁻¹ ≤ c⁻¹ ^ 2 * dist a b

Reciprocation is Lipschitz on real numbers bounded below by a positive constant.

theorem LipschitzWith.inv_of_pos_lower_bound {X : Type u_2} [PseudoMetricSpace X] {f : X → ℝ} {K : NNReal} (hf : LipschitzWith K f) {c : ℝ} (hc : 0 < c) (hbound : ∀ (x : X), c ≤ f x) :

LipschitzWith ((c⁻¹ ^ 2).toNNReal * K) fun (x : X) => (f x)⁻¹

The reciprocal of a positive uniformly bounded-below Lipschitz function is Lipschitz.

theorem Convex.exists_lipschitzWith_inv_gauge_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) {R : ℝ} (hR : 0 < R) (hbound : s ⊆ Metric.closedBall 0 R) :

∃ (C : NNReal), LipschitzWith C fun (u : ↑{u : E | ‖u‖ = 1}) => (gauge s ↑u)⁻¹

The reciprocal gauge is Lipschitz on the unit sphere of a bounded convex neighborhood of zero.

theorem Convex.exists_lipschitzWith_radial_gauge_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) {R : ℝ} (hR : 0 < R) (hbound : s ⊆ Metric.closedBall 0 R) :

∃ (C : NNReal), LipschitzWith C fun (u : ↑{u : E | ‖u‖ = 1}) => (gauge s ↑u)⁻¹ • ↑u

Radial gauge rescaling is Lipschitz on the unit sphere.

For Mathlib / Analysis / Convex / Gauge Rescale #

noncomputable def radialGaugeHomeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) (hb : Bornology.IsVonNBounded ℝ s) :

↑{u : E | ‖u‖ = 1} ≃ₜ ↑(frontier s)

Gauge rescaling identifies the unit sphere with the frontier of a bounded convex neighborhood.

Equations

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

Instances For

theorem radialGaugeHomeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) (hb : Bornology.IsVonNBounded ℝ s) (u : ↑{u : E | ‖u‖ = 1}) :

↑((radialGaugeHomeomorph hs h₀ hb) u) = (gauge s ↑u)⁻¹ • ↑u

The radial gauge homeomorphism sends a unit vector to its reciprocal-gauge multiple.

noncomputable def translatedRadialGaugeHomeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) (hb : Bornology.IsVonNBounded ℝ s) (o : E) :

↑{u : E | ‖u‖ = 1} ≃ₜ ↑(frontier (o +ᵥ s))

Translate the radial gauge homeomorphism by a fixed vector.

Equations

translatedRadialGaugeHomeomorph hs h₀ hb o = (radialGaugeHomeomorph hs h₀ hb).trans (((Homeomorph.addLeft o).image (frontier s)).trans (Homeomorph.setCongr ⋯))

Instances For

theorem translatedRadialGaugeHomeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) (hb : Bornology.IsVonNBounded ℝ s) (o : E) (u : ↑{u : E | ‖u‖ = 1}) :

↑((translatedRadialGaugeHomeomorph hs h₀ hb o) u) = o + (gauge s ↑u)⁻¹ • ↑u

The translated radial gauge homeomorphism has the expected affine formula.

theorem exists_lipschitzWith_translatedRadialGaugeHomeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (h₀ : s ∈ nhds 0) (hb : Bornology.IsVonNBounded ℝ s) (o : E) {R : ℝ} (hR : 0 < R) (hbound : s ⊆ Metric.closedBall 0 R) :

∃ (C : NNReal), LipschitzWith C fun (u : ↑{u : E | ‖u‖ = 1}) => ↑((translatedRadialGaugeHomeomorph hs h₀ hb o) u)

The translated radial gauge homeomorphism is Lipschitz on the unit sphere.

theorem exists_radial_homeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (hb : Bornology.IsBounded s) (o : E) (ho : o ∈ interior s) :

∃ (ρ : E → ℝ) (e : ↑{u : E | ‖u‖ = 1} ≃ₜ ↑(frontier s)) (C : NNReal), (∀ (u : E), ‖u‖ = 1 → 0 < ρ u ∧ o + ρ u • u ∈ frontier s ∧ ∀ (r : ℝ), 0 < r → o + r • u ∈ frontier s → r = ρ u) ∧ (∀ (u : ↑{u : E | ‖u‖ = 1}), ↑(e u) = o + ρ ↑u • ↑u) ∧ LipschitzWith C fun (u : ↑{u : E | ‖u‖ = 1}) => ↑(e u)

A bounded convex set with an interior basepoint admits a positive Lipschitz radial parametrization of its frontier.

Radial exit points of a convex set #

From an interior base point of a compact convex set, every point of the set lies on a segment ending at a boundary point, and that boundary point is unique. These are the facts behind a radial decomposition of a convex body into cones over its boundary.

theorem Convex.mem_interior_of_sub_eq_smul_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) {o w z : E} {γ : ℝ} (ho : o ∈ interior s) (hw : w ∈ s) (hγ₀ : 0 ≤ γ) (hγ₁ : γ < 1) (h : z - o = γ • (w - o)) :

z ∈ interior s

A point lying a fixed fraction of the way, less than all of it, from an interior point of a convex set towards a point of the set is itself an interior point.

theorem Convex.exists_mem_frontier_mem_segment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {s : Set E} (hs : Convex ℝ s) (hcomp : IsCompact s) {o : E} (ho : o ∈ interior s) {x : E} (hx : x ∈ s) :

∃ p ∈ frontier s, x ∈ segment ℝ o p

From an interior base point, every point of a compact convex set lies on a segment ending at a boundary point: the radial exit point of its direction.

theorem Convex.eq_of_mem_frontier_of_mem_segment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) (hclosed : IsClosed s) {o x z w : E} (ho : o ∈ interior s) (hxo : x ≠ o) (hz : z ∈ frontier s) (hw : w ∈ frontier s) (hxz : x ∈ segment ℝ o z) (hxw : x ∈ segment ℝ o w) :

z = w

The radial exit point from an interior base point is unique.

For Mathlib / Analysis / Finite Envelope #

theorem List.abs_foldr_min_apply_sub_le (l : List (ℝ → ℝ)) (r L x z : ℝ) (hL : 0 ≤ L) (hl : ∀ f ∈ l, |f x - f z| ≤ L * |x - z|) :

|foldr (fun (f : ℝ → ℝ) (s : ℝ) => min (f x) s) r l - foldr (fun (f : ℝ → ℝ) (s : ℝ) => min (f z) s) r l| ≤ L * |x - z|

theorem List.abs_foldr_max_apply_sub_le (l : List (ℝ → ℝ)) (r L x z : ℝ) (hL : 0 ≤ L) (hl : ∀ f ∈ l, |f x - f z| ≤ L * |x - z|) :

|foldr (fun (f : ℝ → ℝ) (s : ℝ) => max (f x) s) r l - foldr (fun (f : ℝ → ℝ) (s : ℝ) => max (f z) s) r l| ≤ L * |x - z|

theorem List.le_foldr_min_apply_iff (l : List (ℝ → ℝ)) (r x y : ℝ) :

y ≤ foldr (fun (f : ℝ → ℝ) (s : ℝ) => min (f x) s) r l ↔ y ≤ r ∧ ∀ f ∈ l, y ≤ f x

theorem List.foldr_max_apply_le_iff (l : List (ℝ → ℝ)) (r x y : ℝ) :

foldr (fun (f : ℝ → ℝ) (s : ℝ) => max (f x) s) r l ≤ y ↔ r ≤ y ∧ ∀ f ∈ l, f x ≤ y

For Mathlib / Analysis / Inner Product Space / Box #

theorem EuclideanSpace.isBounded_coordinate_rectangle (l r a b : ℝ) :

Bornology.IsBounded {p : EuclideanSpace ℝ (Fin 2) | l ≤ p.ofLp 0 ∧ p.ofLp 0 ≤ r ∧ a ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ b}

A rectangle with finite coordinate bounds is bounded in the Euclidean plane.

Linearity of a real inner product in its left argument #

Mathlib.Analysis.InnerProductSpace.Basic provides the continuous linear map innerSL ℝ v = fun x ↦ ⟪v, x⟫; the bundled form of the symmetric slot is what the half-space convexity lemmas convex_halfSpace_le and convex_halfSpace_ge consume.

theorem isLinearMap_inner_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) :

IsLinearMap ℝ fun (x : E) => inner ℝ x v

x ↦ ⟪x, v⟫ is a linear map of a real inner product space.

For Mathlib / Analysis / Normed / Affine / Continuous Affine Map #

theorem ContinuousAffineMap.continuous_comp_right {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] (g : E →ᴬ[ℝ ] F) :

Continuous fun (f : F →ᴬ[ℝ ] G) => f.comp g

Precomposition by a fixed continuous affine map is continuous.

For Mathlib / Analysis / Special Functions / Angle #

theorem Real.Angle.coe_ne_coe_of_abs_sub_lt {x y : ℝ} (hne : x ≠ y) (h : |x - y| < 2 * Real.pi) :

↑x ≠ ↑y

Distinct reals at distance less than a full turn have distinct angles.

For Mathlib / Analysis / Special Functions / Angle Lift #

theorem Real.sub_eq_sub_of_cos_eq_cos_of_sin_eq_sin {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] {θ ψ : X → ℝ} (hθ : Continuous θ) (hψ : Continuous ψ) (hcos : ∀ (x : X), cos (θ x) = cos (ψ x)) (hsin : ∀ (x : X), sin (θ x) = sin (ψ x)) (x y : X) :

θ x - ψ x = θ y - ψ y

Continuous real angle lifts of the same circle-valued map differ by a constant.

A cubic remainder bound for the arctangent #

Real.abs_arctan_sub_self_le complements Real.abs_arctan_le_abs by quantifying the first-order approximation arctan s ≈ s near the origin.

theorem Real.abs_arctan_sub_self_le (s : ℝ) :

|arctan s - s| ≤ |s| ^ 3

The arctangent differs from the identity by at most a cubic error.

theorem Real.abs_arctan_div_sub_le_of_small {w0 w1 d0 d1 nw nd : ℝ} (hnw : 0 < nw) (hnw2 : nw ^ 2 = w0 ^ 2 + w1 ^ 2) (hnd : 0 ≤ nd) (hnd2 : nd ^ 2 = d0 ^ 2 + d1 ^ 2) (hsmall : 2 * nd ≤ nw) :

|arctan ((w0 * d1 - w1 * d0) / (nw ^ 2 + (w0 * d0 + w1 * d1))) - (w0 * d1 - w1 * d0) / nw ^ 2| ≤ 6 * nd ^ 2 / nw ^ 2

First-order angle estimate. If W = (w0, w1) has norm nw > 0 and the displacement d = (d0, d1) has norm nd with 2 * nd ≤ nw, then the principal angle between W and W + d, in the arctangent form given by their cross and dot products, differs from its linearization (w0 * d1 - w1 * d0) / nw ^ 2 by at most 6 * nd ^ 2 / nw ^ 2.

Two-sided bracketing of an alternating series with an antitone tail #

alternating_series_bracket_of_antitone_shift upgrades the one-sided Leibniz estimates Antitone.alternating_series_le_tendsto and Antitone.tendsto_le_alternating_series to a two-sided bracket for an alternating series whose term magnitudes are antitone only from an even index 2 * N onwards: the sum then lies between the partial sums of 2 * N and of 2 * N + 1 terms. antitone_pow_div_factorial_two_mul_add is the antitonicity criterion for the stride-two factorial quotients x ^ (2 * n + a) / (2 * n + a)! that the Taylor series of the trigonometric functions produce.

theorem antitone_pow_div_factorial_two_mul_add {x : ℝ} (hx0 : 0 ≤ x) {a : ℕ} (hx : x ^ 2 ≤ ↑((a + 1) * (a + 2))) :

Antitone fun (n : ℕ) => x ^ (2 * n + a) / ↑(2 * n + a).factorial

The stride-two factorial quotients x ^ (2 * n + a) / (2 * n + a)! are antitone as soon as x ^ 2 ≤ (a + 1) * (a + 2), i.e. as soon as the first term ratio is at most one.

theorem alternating_series_bracket_of_antitone_shift {f : ℕ → ℝ} {l : ℝ} (N : ℕ) (hfl : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfa : Antitone fun (n : ℕ) => f (2 * N + n)) :

∑ i ∈ Finset.range (2 * N), (-1) ^ i * f i ≤ l ∧ l ≤ ∑ i ∈ Finset.range (2 * N + 1), (-1) ^ i * f i

Leibniz bracketing for an alternating series whose term magnitudes are antitone only from index 2 * N onwards: the limit lies between the partial sums of 2 * N and of 2 * N + 1 terms.

For Mathlib / Analysis / Special Functions / Trigonometric #

theorem Real.tan_pi_div_two_sub_div_two (ω : ℝ) (hω : ω ∈ Set.Ico 0 (Real.pi / 2)) :

tan ((Real.pi / 2 - ω) / 2) = (cos ω)⁻¹ - tan ω

The tangent of half a complementary angle is secant minus tangent on the first quadrant.

theorem Real.antitoneOn_cos_div_sin_Ioo_neg_pi_zero :

AntitoneOn (fun (x : ℝ) => cos x / sin x) (Set.Ioo (-Real.pi) 0)

Cotangent is antitone between its consecutive poles at negative pi and zero.

theorem Real.tan_le_self_add_cube {x : ℝ} (hx : 0 ≤ x) (hx1 : x ≤ 1) :

tan x ≤ x + 4 / 3 * x ^ 3

A cubic upper bound for the tangent on [0, 1], companion to Real.sin_gt_sub_cube.

theorem Real.sin_mem_Icc_taylor_sums (N : ℕ) {x : ℝ} (hx0 : 0 ≤ x) (hx : x ^ 2 ≤ ↑((4 * N + 2) * (4 * N + 3))) :

sin x ∈ Set.Icc (∑ k ∈ Finset.range (2 * N), (-1) ^ k * x ^ (2 * k + 1) / ↑(2 * k + 1).factorial) (∑ k ∈ Finset.range (2 * N + 1), (-1) ^ k * x ^ (2 * k + 1) / ↑(2 * k + 1).factorial)

Leibniz bracketing of the sine by its Maclaurin partial sums: for 0 ≤ x with x ^ 2 ≤ (4 * N + 2) * (4 * N + 3) the value Real.sin x lies between the partial sums of 2 * N and of 2 * N + 1 terms, the first of which undershoots and the second overshoots.

theorem Real.cos_mem_Icc_taylor_sums (N : ℕ) {x : ℝ} (hx0 : 0 ≤ x) (hx : x ^ 2 ≤ ↑((4 * N + 1) * (4 * N + 2))) :

cos x ∈ Set.Icc (∑ k ∈ Finset.range (2 * N), (-1) ^ k * x ^ (2 * k) / ↑(2 * k).factorial) (∑ k ∈ Finset.range (2 * N + 1), (-1) ^ k * x ^ (2 * k) / ↑(2 * k).factorial)

Leibniz bracketing of the cosine by its Maclaurin partial sums: for 0 ≤ x with x ^ 2 ≤ (4 * N + 1) * (4 * N + 2) the value Real.cos x lies between the partial sums of 2 * N and of 2 * N + 1 terms, the first of which undershoots and the second overshoots.

ForMathlib.BoundedVariation.

For Mathlib / Bounded Variation #

theorem eVariationOn.add_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] (f g : α → E) (s : Set α) :

eVariationOn (f + g) s ≤ eVariationOn f s + eVariationOn g s

The variation of a sum is at most the sum of the variations.

theorem BoundedVariationOn.add {α : Type u_1} {E : Type u_2} [LinearOrder α] [SeminormedAddCommGroup E] {f g : α → E} {s : Set α} (hf : BoundedVariationOn f s) (hg : BoundedVariationOn g s) :

BoundedVariationOn (f + g) s

A sum of two functions of bounded variation has bounded variation.

theorem eVariationOn.sum_edist_fin_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [PseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ} (u : Fin (n + 1) → α) (hu : Monotone u) (hus : ∀ (i : Fin (n + 1)), u i ∈ s) :

∑ i : Fin n, edist (f (u i.succ)) (f (u i.castSucc)) ≤ eVariationOn f s

Variation bounds the increments along a finite monotone partition.

theorem BoundedVariationOn.sum_norm_sub_fin_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [NormedAddCommGroup E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {n : ℕ} (u : Fin (n + 1) → α) (hu : Monotone u) (hus : ∀ (i : Fin (n + 1)), u i ∈ s) :

∑ i : Fin n, ‖f (u i.succ) - f (u i.castSucc)‖ ≤ (eVariationOn f s).toReal

Total variation bounds the sum of norms of increments on a finite partition.

theorem BoundedVariationOn.sum_norm_sub_sq_fin_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [NormedAddCommGroup E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {n : ℕ} (u : Fin (n + 1) → α) (hu : Monotone u) (hus : ∀ (i : Fin (n + 1)), u i ∈ s) {δ : ℝ} (hδ : 0 ≤ δ) (hbound : ∀ (i : Fin n), ‖f (u i.succ) - f (u i.castSucc)‖ ≤ δ) :

∑ i : Fin n, ‖f (u i.succ) - f (u i.castSucc)‖ ^ 2 ≤ δ * (eVariationOn f s).toReal

Squared increments are bounded by the largest increment times the total variation.

theorem BoundedVariationOn.abs_sub_sum_le_of_param_quadratic_remainder {α : Type u_1} {E : Type u_2} [LinearOrder α] [NormedAddCommGroup E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {n : ℕ} (u : Fin (n + 1) → α) (hu : Monotone u) (hus : ∀ (i : Fin (n + 1)), u i ∈ s) (A : α → ℝ) (L : Fin n → ℝ) {C δ : ℝ} (hC : 0 ≤ C) (hδ : 0 ≤ δ) (hbound : ∀ (i : Fin n), ‖f (u i.succ) - f (u i.castSucc)‖ ≤ δ) (herror : ∀ (i : Fin n), |A (u i.succ) - A (u i.castSucc) - L i| ≤ C * ‖f (u i.succ) - f (u i.castSucc)‖ ^ 2) :

|A (u (Fin.last n)) - A (u 0) - ∑ i : Fin n, L i| ≤ C * δ * (eVariationOn f s).toReal

A telescoping sum of increments with quadratic remainders is controlled by the largest increment times the total variation.

theorem BoundedVariationOn.tendsto_sum_of_local_quadratic_remainder {E : Type u_1} [NormedAddCommGroup E] {a b : ℝ} (hab : a ≤ b) {f : ↑(Set.Icc a b) → E} (hf : BoundedVariationOn f Set.univ) (hfc : Continuous f) (A : ↑(Set.Icc a b) → ℝ) (L : ↑(Set.Icc a b) → E → ℝ) {C : ℝ} (hC : 0 ≤ C) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (herror : ∀ (t u : ↑(Set.Icc a b)), ↑t ≤ ↑u → ↑u - ↑t < δ₀ → |A u - A t - L t (f u - f t)| ≤ C * ‖f u - f t‖ ^ 2) (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), L (cuts k i.castSucc) (f (cuts k i.succ) - f (cuts k i.castSucc))) Filter.atTop (nhds (A ⟨b, ⋯⟩ - A ⟨a, ⋯⟩))

If the increments of a real function A agree with a linear functional of the increments of a bounded variation path up to a quadratic remainder on all parameter pairs closer than a fixed positive threshold, then the linear sums along any family of partitions whose mesh tends to zero converge to the endpoint increment of A.

theorem BoundedVariationOn.Icc_union_Icc {α : Type u_1} {E : Type u_2} [LinearOrder α] [PseudoEMetricSpace E] {f : α → E} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) (h₁ : BoundedVariationOn f (Set.Icc a b)) (h₂ : BoundedVariationOn f (Set.Icc b c)) :

BoundedVariationOn f (Set.Icc a c)

Bounded variation on two adjacent closed intervals gives bounded variation on their union.

theorem BoundedVariationOn.univ_of_Icc_endpoints {α : Type u_1} {E : Type u_2} [LinearOrder α] [PseudoEMetricSpace E] {a b : α} (hab : a ≤ b) {g : ↑(Set.Icc a b) → E} (h : BoundedVariationOn g (Set.Icc ⟨a, ⋯⟩ ⟨b, ⋯⟩)) :

BoundedVariationOn g Set.univ

A function on the order subtype Set.Icc a b has bounded variation everywhere as soon as it has bounded variation on the closed interval between the two endpoints of that subtype.

ForMathlib.Convex.Body.BoundaryMeasure.
ForMathlib.Convex.Body.Hausdorff.
ForMathlib.Convex.Collinear.
ForMathlib.Convex.Body.Segment.
ForMathlib.Convex.Function.
ForMathlib.Convex.Hausdorff.
ForMathlib.Convex.Support.
ForMathlib.Convex.Translation.

For Mathlib / Convex / Body / Boundary Measure #

theorem ConvexBody.hausdorffMeasure_frontier_lt_top (K : ConvexBody (EuclideanSpace ℝ (Fin 2))) (hint : (interior ↑K).Nonempty) :

(MeasureTheory.Measure.hausdorffMeasure 1) (frontier ↑K) < ⊤

The frontier of a planar convex body with nonempty interior has finite one-dimensional Hausdorff measure.

For Mathlib / Convex / Body / Hausdorff #

theorem ConvexBody.mem_of_tendsto_hausdorffDist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (q : E) (K : ℕ → ConvexBody E) (L : ConvexBody E) (hev : ∀ᶠ (n : ℕ) in Filter.atTop , q ∈ ↑(K n)) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) :

q ∈ ↑L

Eventual membership persists in a Hausdorff limit of convex bodies.

For Mathlib / Convex / Collinear #

theorem Convex.collinear_of_interior_eq_empty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : Convex ℝ s) (hdim : Module.finrank ℝ E ≤ 2) (hint : interior s = ∅) :

Collinear ℝ s

A convex set with empty interior in dimension at most two is collinear.

theorem Collinear.mem_segment_of_apply_le {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Collinear ℝ s) {a p x : E} (ha : a ∈ s) (hp : p ∈ s) (hx : x ∈ s) (f : E →ₗ[ℝ ] ℝ) (hpos : 0 < f (p - a)) (hle : f p ≤ f x) :

p ∈ segment ℝ a x

A separating linear functional orders points on a line into a segment.

For Mathlib / Convex / Body / Segment #

theorem ConvexBody.exists_eq_segment_of_interior_empty (K : ConvexBody (EuclideanSpace ℝ (Fin 2))) (hsub : ¬(↑K).Subsingleton) (hint : interior ↑K = ∅) :

∃ (a : EuclideanSpace ℝ (Fin 2)) (b : EuclideanSpace ℝ (Fin 2)), a ≠ b ∧ ↑K = segment ℝ a b

A nonsingleton planar convex body with empty interior is a nontrivial segment.

For Mathlib / Convex / Function #

theorem ConvexOn.lt_on_Ico_of_lt_of_le {f : ℝ → ℝ} {a b t c : ℝ} (hf : ConvexOn ℝ (Set.Icc a b) f) (ha : f a < c) (hb : f b ≤ c) (hat : a ≤ t) (htb : t < b) :

f t < c

A convex function stays below a bound before the right endpoint if the left endpoint is strictly below the bound and the right endpoint is at most the bound.

For Mathlib / Convex / Hausdorff #

theorem TopologicalSpace.NonemptyCompacts.convex_of_tendsto {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter ι} [l.NeBot] {K : ι → NonemptyCompacts E} {L : NonemptyCompacts E} (hK : ∀ (n : ι), Convex ℝ ↑(K n)) (hlim : Filter.Tendsto K l (nhds L)) :

Convex ℝ ↑L

Hausdorff limits of nonempty compact convex sets are convex.

For Mathlib / Convex / Support #

theorem IsCompact.abs_csSup_inner_sub_le_hausdorffDist {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S T : Set E} (hS : IsCompact S) (hneS : S.Nonempty) (hT : IsCompact T) (hneT : T.Nonempty) (u : E) :

|sSup ((fun (x : E) => inner ℝ x u) '' S) - sSup ((fun (x : E) => inner ℝ x u) '' T)| ≤ Metric.hausdorffDist S T * ‖u‖

Support values of compact sets differ by at most their Hausdorff distance times the norm of the direction.

theorem IsCompact.abs_csSup_inner_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : IsCompact S) (hneS : S.Nonempty) (u v : E) :

|sSup ((fun (x : E) => inner ℝ x u) '' S) - sSup ((fun (x : E) => inner ℝ x v) '' S)| ≤ sSup (norm '' S) * ‖u - v‖

The support values of a compact set are Lipschitz in the direction, with constant equal to the maximum norm of a point in the set.

theorem ConvexBody.eq_iInter_halfSpaces {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) :

↑K = ⋂ u ∈ {u : E | ‖u‖ = 1}, {p : E | inner ℝ p u ≤ sSup ((fun (x : E) => inner ℝ x u) '' ↑K)}

A convex body in a real inner product space is the intersection of its supporting half-spaces.

For Mathlib / Convex / Translation #

def ConvexBody.translate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) (v : E) :

ConvexBody E

Translation of a convex body by a vector.

Equations

K.translate v = { carrier := (fun (p : E) => p + v) '' ↑K, convex' := ⋯, isCompact' := ⋯, nonempty' := ⋯ }

Instances For

ForMathlib.Geometry.Euclidean.Segment.

For Mathlib / Geometry / Euclidean / Segment #

theorem EuclideanGeometry.eq_or_eq_neg_of_unit_orthogonal (o : Orientation ℝ (EuclideanSpace ℝ (Fin 2)) (Fin 2)) {v n m : EuclideanSpace ℝ (Fin 2)} (hv : v ≠ 0) (hn : ‖n‖ = 1) (hm : ‖m‖ = 1) (hvn : inner ℝ v n = 0) (hvm : inner ℝ v m = 0) :

n = m ∨ n = -m

Two unit vectors perpendicular to the same nonzero planar vector agree up to sign.

theorem EuclideanGeometry.inner_direction_eq_zero_of_segment_eq {a b c d n : EuclideanSpace ℝ (Fin 2)} (hseg : segment ℝ a b = segment ℝ c d) (hcdn : inner ℝ (d - c) n = 0) :

inner ℝ (b - a) n = 0

Equal segments have the same orthogonal directions.

theorem EuclideanGeometry.dist_eq_of_segment_eq {a b c d : EuclideanSpace ℝ (Fin 2)} (hseg : segment ℝ a b = segment ℝ c d) :

dist a b = dist c d

Equal segments have equal endpoint distances.

theorem EuclideanGeometry.segment_inter_hyperplane_subsingleton {a b n : EuclideanSpace ℝ (Fin 2)} {c : ℝ} (h : inner ℝ (b - a) n ≠ 0) :

(segment ℝ a b ∩ {q : EuclideanSpace ℝ (Fin 2) | inner ℝ q n = c}).Subsingleton

A segment transverse to a hyperplane meets it in at most one point.

theorem EuclideanGeometry.hausdorffMeasure_segment_inter_hyperplane_eq_zero {a b n : EuclideanSpace ℝ (Fin 2)} {c : ℝ} (h : inner ℝ (b - a) n ≠ 0) :

(MeasureTheory.Measure.hausdorffMeasure 1) (segment ℝ a b ∩ {q : EuclideanSpace ℝ (Fin 2) | inner ℝ q n = c}) = 0

A transverse segment has zero length on a hyperplane.

theorem EuclideanGeometry.segment_inter_hyperplane_subsingleton_of_not_subset {a b n : EuclideanSpace ℝ (Fin 2)} {c : ℝ} (hnot : ¬segment ℝ a b ⊆ {q : EuclideanSpace ℝ (Fin 2) | inner ℝ q n = c}) :

(segment ℝ a b ∩ {q : EuclideanSpace ℝ (Fin 2) | inner ℝ q n = c}).Subsingleton

A segment not contained in a hyperplane meets it in at most one point.

theorem EuclideanGeometry.exists_segment_subset_hyperplane_of_finite_cover {ι : Type u_1} (I : Finset ι) (n : ι → EuclideanSpace ℝ (Fin 2)) (c : ι → ℝ) {a b : EuclideanSpace ℝ (Fin 2)} (hab : a ≠ b) (hcover : segment ℝ a b ⊆ ⋃ i ∈ I, {q : EuclideanSpace ℝ (Fin 2) | inner ℝ q (n i) = c i}) :

∃ i ∈ I, segment ℝ a b ⊆ {q : EuclideanSpace ℝ (Fin 2) | inner ℝ q (n i) = c i}

A nondegenerate segment covered by finitely many hyperplanes lies in one of them.

ForMathlib.MeasureTheory.EuclideanSpace.
ForMathlib.MeasureTheory.FiniteMeasure.Portmanteau.
ForMathlib.MeasureTheory.FiniteMeasure.Restriction.
ForMathlib.MeasureTheory.Angle.
ForMathlib.MeasureTheory.Hausdorff.Arclength.
ForMathlib.MeasureTheory.Hausdorff.Graph.
ForMathlib.MeasureTheory.Hausdorff.PlanarGraph.
ForMathlib.MeasureTheory.Integral.AtomicBounds.
ForMathlib.MeasureTheory.Integral.IntervalExhaustion.
ForMathlib.MeasureTheory.Integral.MovingIntervals.
ForMathlib.MeasureTheory.Integral.Translation.
ForMathlib.MeasureTheory.Measure.Atoms.
ForMathlib.MeasureTheory.Measure.HaarNullSets.
ForMathlib.MeasureTheory.Measure.Map.
ForMathlib.MeasureTheory.Measure.WithDensity.
ForMathlib.MeasureTheory.RegionBetween.
ForMathlib.MeasureTheory.Measure.PlanarTrapezoid.
ForMathlib.MeasureTheory.Measure.PlanarTriangle.
ForMathlib.MeasureTheory.StieltjesDensity.
ForMathlib.MeasureTheory.VectorMeasure.Interval.
ForMathlib.MeasureTheory.VectorMeasure.WithDensity.
ForMathlib.MeasureTheory.Volume.

For Mathlib / Measure Theory / Euclidean Space #

theorem EuclideanSpace.volume_preserving_finTwoCoordinates :

MeasureTheory.MeasurePreserving (fun (p : EuclideanSpace ℝ (Fin 2)) => (p.ofLp 0, p.ofLp 1)) MeasureTheory.volume MeasureTheory.volume

theorem EuclideanSpace.volume_setOf_apply_mem_Icc (l r b t : ℝ) :

MeasureTheory.volume {p : EuclideanSpace ℝ (Fin 2) | p.ofLp 0 ∈ Set.Icc l r ∧ p.ofLp 1 ∈ Set.Icc b t} = ENNReal.ofReal (r - l) * ENNReal.ofReal (t - b)

The volume of a closed coordinate box of the Euclidean plane.

def EuclideanSpace.finTwoCoordinatesSwap (p : EuclideanSpace ℝ (Fin 2)) :

ℝ × ℝ

The coordinates of a point of the Euclidean plane, listed second coordinate first.

Equations

p.finTwoCoordinatesSwap = (p.ofLp 1, p.ofLp 0)

Instances For

MeasureTheory.MeasurePreserving finTwoCoordinatesSwap MeasureTheory.volume (MeasureTheory.volume.prod MeasureTheory.volume)

theorem EuclideanSpace.volume_preserving_finTwoCoordinatesSwap :

Reading the plane coordinates in the reversed order is measure preserving.

Portmanteau for finite measures: the open-set inequality #

Mathlib proves the open-set portmanteau inequality MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto for probability measures and only the closed-set inequality MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto for finite measures. This file supplies the missing open-set inequality for finite measures, by combining the closed-set inequality on the complement with the convergence of the total masses.

theorem MeasureTheory.FiniteMeasure.le_liminf_measure_open_of_tendsto {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [OpensMeasurableSpace Ω] {μ : FiniteMeasure Ω} {μs : ι → FiniteMeasure Ω} (hlim : Filter.Tendsto μs L (nhds μ)) {G : Set Ω} (hG : IsOpen G) :

↑μ G ≤ Filter.liminf (fun (i : ι) => ↑(μs i) G) L

Portmanteau for finite measures: weak convergence bounds the mass of an open set by the lower limit of the approximating masses.

For Mathlib / Measure Theory / Finite Measure / Restriction #

theorem MeasureTheory.FiniteMeasure.tendsto_restrict_compl_of_tendsto_restrict {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {F : Filter ι} {μs : ι → FiniteMeasure X} {μ : FiniteMeasure X} {s : Set X} (hs : MeasurableSet s) (hμ : Filter.Tendsto μs F (nhds μ)) (hsμ : Filter.Tendsto (fun (n : ι) => (μs n).restrict s) F (nhds (μ.restrict s))) :

Filter.Tendsto (fun (n : ι) => (μs n).restrict sᶜ) F (nhds (μ.restrict sᶜ))

Weak convergence of finite measures and their restrictions implies weak convergence of the complementary restrictions.

theorem MeasureTheory.FiniteMeasure.tendsto_apply_of_null_frontier {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [HasOuterApproxClosed X] [Nonempty X] {F : Filter ι} {μs : ι → FiniteMeasure X} {μ : FiniteMeasure X} {s : Set X} (hμ : Filter.Tendsto μs F (nhds μ)) (hs : μ (frontier s) = 0) :

Filter.Tendsto (fun (n : ι) => (μs n) s) F (nhds (μ s))

A continuity set has convergent masses under weak convergence of finite measures.

theorem MeasureTheory.Measure.restrict_finset_eq_of_singleton_eq {X : Type u_1} [MeasurableSpace X] [MeasurableSingletonClass X] {μ ν : Measure X} (s : Finset X) (h : ∀ x ∈ s, μ {x} = ν {x}) :

μ.restrict ↑s = ν.restrict ↑s

Equal atoms on a finite set give equal restrictions to that set.

theorem MeasureTheory.FiniteMeasure.tendsto_restrict_compl_finset_of_singleton_eq {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [MeasurableSingletonClass X] {F : Filter ι} {μs : ι → FiniteMeasure X} {μ : FiniteMeasure X} (s : Finset X) (hμ : Filter.Tendsto μs F (nhds μ)) (h : ∀ (n : ι), ∀ x ∈ s, ↑(μs n) {x} = ↑μ {x}) :

Filter.Tendsto (fun (n : ι) => (μs n).restrict (↑s)ᶜ) F (nhds (μ.restrict (↑s)ᶜ))

Removing finitely many fixed atoms preserves weak convergence.

theorem MeasureTheory.FiniteMeasure.tendsto_restrict_of_null_frontier {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [HasOuterApproxClosed X] [Nonempty X] {F : Filter ι} {μs : ι → FiniteMeasure X} {μ : FiniteMeasure X} {s : Set X} (hs : MeasurableSet s) (hμ : Filter.Tendsto μs F (nhds μ)) (hfrontier : μ (frontier s) = 0) :

Filter.Tendsto (fun (n : ι) => (μs n).restrict s) F (nhds (μ.restrict s))

Weak convergence is preserved by restriction to a measurable continuity set.

theorem MeasureTheory.FiniteMeasure.tendsto_restrict_of_frontier_subset_finset {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [HasOuterApproxClosed X] [Nonempty X] [MeasurableSingletonClass X] {F : Filter ι} {μs : ι → FiniteMeasure X} {μ : FiniteMeasure X} {s : Set X} (hs : MeasurableSet s) (t : Finset X) (hfrontier : frontier s ⊆ ↑t) (hμ : Filter.Tendsto μs F (nhds μ)) (hatoms : ∀ (n : ι), ∀ x ∈ t, ↑(μs n) {x} = ↑μ {x}) :

Filter.Tendsto (fun (n : ι) => (μs n).restrict s) F (nhds (μ.restrict s))

Fixed atoms on a finite set containing the frontier allow weak restriction convergence.

For Mathlib / Measure Theory / Angle #

theorem Real.Angle.injOn_coe_Ioc {a b : ℝ} (h : b ≤ a + 2 * Real.pi) :

Set.InjOn (fun (t : ℝ) => ↑t) (Set.Ioc a b)

A half-open interval of at most one turn has distinct angular representatives.

theorem Real.Angle.countable_preimage_coe_singleton (x : Angle) :

((fun (s : ℝ) => ↑s) ⁻¹' {x}).Countable

Every fibre of the angular projection is countable, being a full residue class.

theorem Real.Angle.isOpen_image_Ioo (a b : ℝ) :

IsOpen ((fun (t : ℝ) => ↑t) '' Set.Ioo a b)

The quotient map sends an open real interval to an open angular arc.

theorem Real.Angle.frontier_image_Ioo_subset (a b : ℝ) :

frontier ((fun (t : ℝ) => ↑t) '' Set.Ioo a b) ⊆ {↑a, ↑b}

The frontier of an angular arc is contained in its two endpoint angles.

theorem Real.Angle.image_Ioc_eq_image_Ioo_union {a b : ℝ} (hab : a < b) :

(fun (t : ℝ) => ↑t) '' Set.Ioc a b = (fun (t : ℝ) => ↑t) '' Set.Ioo a b ∪ {↑b}

A nonempty half-open arc consists of its open arc and its terminal angle.

theorem Real.Angle.frontier_image_Ioc_subset {a b : ℝ} (hab : a < b) :

frontier ((fun (t : ℝ) => ↑t) '' Set.Ioc a b) ⊆ {↑a, ↑b}

The frontier of a nonempty half-open angular arc lies in its two endpoint angles.

theorem Real.Angle.measurableSet_image_Ioc [MeasurableSpace Angle] [BorelSpace Angle] (a b : ℝ) :

MeasurableSet ((fun (t : ℝ) => ↑t) '' Set.Ioc a b)

Half-open real intervals have measurable angular images.

theorem Real.Angle.measurableSet_image_of_subset_Ioc [MeasurableSpace Angle] [BorelSpace Angle] {a b : ℝ} (hab : b ≤ a + 2 * Real.pi) {E : Set ℝ} (hE : MeasurableSet E) (hEab : E ⊆ Set.Ioc a b) :

MeasurableSet ((fun (t : ℝ) => ↑t) '' E)

A Borel subset of a real interval of at most one turn has a Borel angular image.

theorem Real.Angle.preimage_sub_pi_image_Ioo (a b : ℝ) :

(fun (t : Angle) => t - ↑Real.pi) ⁻¹' (fun (s : ℝ) => ↑s) '' Set.Ioo a b = (fun (s : ℝ) => ↑s) '' Set.Ioo (a + Real.pi) (b + Real.pi)

The preimage of an open angular arc under the half-turn shift is the shifted arc.

theorem Real.Angle.disjoint_image_Ioo_singleton {a b : ℝ} (h : b ≤ a + 2 * Real.pi) :

Disjoint ((fun (t : ℝ) => ↑t) '' Set.Ioo a b) {↑b}

The terminal atom is disjoint from the open arc, even for a full turn.

theorem Real.Angle.integral_image_Ioc [MeasurableSpace Angle] [BorelSpace Angle] (μ : MeasureTheory.FiniteMeasure Angle) (f : BoundedContinuousFunction Angle ℝ) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) :

∫ (x : Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f x ∂↑μ = ∫ (x : Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioo a b, f x ∂↑μ + (↑μ).real {↑b} * f ↑b

Passing from an open arc to a half-open arc restores exactly its terminal atom.

theorem Real.Angle.tendsto_integral_image_Ioc_of_fixed_endpoint_atoms [MeasurableSpace Angle] [BorelSpace Angle] {ι : Type u_1} {F : Filter ι} {μs : ι → MeasureTheory.FiniteMeasure Angle} {μ : MeasureTheory.FiniteMeasure Angle} {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (hμ : Filter.Tendsto μs F (nhds μ)) (ha : ∀ (n : ι), ↑(μs n) {↑a} = ↑μ {↑a}) (hb : ∀ (n : ι), ↑(μs n) {↑b} = ↑μ {↑b}) (f : BoundedContinuousFunction Angle ℝ) :

Filter.Tendsto (fun (n : ι) => ∫ (x : Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f x ∂↑(μs n)) F (nhds (∫ (x : Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f x ∂↑μ))

Weak convergence with fixed endpoint atoms preserves integrals on half-open angular arcs.

Integration over the circle of directions #

theorem Real.Angle.integrable_of_continuous [MeasurableSpace Angle] [BorelSpace Angle] {E : Type u_1} [NormedAddCommGroup E] {μ : MeasureTheory.Measure Angle} [MeasureTheory.IsFiniteMeasure μ] {f : Angle → E} (hf : Continuous f) :

MeasureTheory.Integrable f μ

A continuous function of a direction is integrable for every finite angular measure, the circle of directions being compact.

Angular measures reading a real density #

theorem Real.Angle.map_coe_withDensity_image_eq_setLIntegral [MeasurableSpace Angle] [BorelSpace Angle] {ν : MeasureTheory.Measure ℝ} {w : ℝ → ENNReal} {S T : Set ℝ} {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) (hS : S ⊆ Set.Ioc a b) (hT : MeasurableSet T) (hTS : T ⊆ S) :

(MeasureTheory.Measure.map (fun (t : ℝ) => ↑t) ((ν.restrict S).withDensity w)) ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, w t ∂ν

On a real window of at most one turn, the pushforward of a weighted measure along the angular projection gives the angular image of a measurable subset the integral of the weight over that subset.

theorem Real.Angle.measure_restrict_image_congr [MeasurableSpace Angle] [BorelSpace Angle] {μ ν : MeasureTheory.Measure Angle} {J : Set ℝ} (hJ : MeasurableSet J) (h : ∀ (T : Set ℝ), MeasurableSet T → T ⊆ J → μ ((fun (t : ℝ) => ↑t) '' T) = ν ((fun (t : ℝ) => ↑t) '' T)) :

μ.restrict ((fun (t : ℝ) => ↑t) '' J) = ν.restrict ((fun (t : ℝ) => ↑t) '' J)

Two angular measures that agree on the angular image of every measurable subset of a real window agree after restriction to that window's angular image.

theorem Real.Angle.measure_restrict_image_congr_of_ae_eq [MeasurableSpace Angle] [BorelSpace Angle] {μ ν : MeasureTheory.Measure Angle} {ρ : MeasureTheory.Measure ℝ} {w w' : ℝ → ENNReal} {J : Set ℝ} (hJ : MeasurableSet J) (hμ : ∀ (T : Set ℝ), MeasurableSet T → T ⊆ J → μ ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, w t ∂ρ) (hν : ∀ (T : Set ℝ), MeasurableSet T → T ⊆ J → ν ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, w' t ∂ρ) (hw : ∀ᵐ (t : ℝ) ∂ρ.restrict J, w t = w' t) :

μ.restrict ((fun (t : ℝ) => ↑t) '' J) = ν.restrict ((fun (t : ℝ) => ↑t) '' J)

Two angular measures reading extended-real weights on a real window agree after restriction to its angular image as soon as the weights agree almost everywhere on the window.

theorem Real.Angle.measure_restrict_image_congr_add [MeasurableSpace Angle] [BorelSpace Angle] {μ ν₁ ν₂ : MeasureTheory.Measure Angle} {ρ : MeasureTheory.Measure ℝ} {f g h : ℝ → ℝ} {J : Set ℝ} (hJ : MeasurableSet J) (hμ : ∀ (T : Set ℝ), MeasurableSet T → T ⊆ J → μ ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, ENNReal.ofReal (h t) ∂ρ) (hν₁ : ∀ (T : Set ℝ), MeasurableSet T → T ⊆ J → ν₁ ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, ENNReal.ofReal (f t) ∂ρ) (hν₂ : ∀ (T : Set ℝ), MeasurableSet T → T ⊆ J → ν₂ ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, ENNReal.ofReal (g t) ∂ρ) (hf : AEMeasurable f (ρ.restrict J)) (hf0 : ∀ᵐ (t : ℝ) ∂ρ.restrict J, 0 ≤ f t) (hg0 : ∀ᵐ (t : ℝ) ∂ρ.restrict J, 0 ≤ g t) (hfg : ∀ᵐ (t : ℝ) ∂ρ.restrict J, h t = f t + g t) :

μ.restrict ((fun (t : ℝ) => ↑t) '' J) = (ν₁ + ν₂).restrict ((fun (t : ℝ) => ↑t) '' J)

An angular measure reading a real density on a window agrees, after restriction to the window's angular image, with a sum of two angular measures whose densities add up to it almost everywhere.

For Mathlib / Measure Theory / Hausdorff / Arclength #

theorem MeasureTheory.hausdorffMeasure_image_Icc_eq_eVariationOn (γ : ℝ → EuclideanSpace ℝ (Fin 2)) {a b : ℝ} (hab : a ≤ b) (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Icc a b)) (hBV : BoundedVariationOn γ (Set.Icc a b)) :

(Measure.hausdorffMeasure 1) (γ '' Set.Icc a b) = eVariationOn γ (Set.Icc a b)

Hausdorff length of a continuous injective arc is its total variation.

theorem MeasureTheory.integrableOn_deriv_of_lipschitzOn {γ : ℝ → EuclideanSpace ℝ (Fin 2)} {C : NNReal} {a b : ℝ} (hγ : LipschitzOnWith C γ (Set.Icc a b)) :

IntegrableOn (deriv γ) (Set.Icc a b) volume

The derivative of a planar Lipschitz curve is integrable on its interval.

theorem MeasureTheory.eVariationOn_eq_ofReal_integral_norm_deriv {γ : ℝ → EuclideanSpace ℝ (Fin 2)} {C : NNReal} {a b : ℝ} (hab : a ≤ b) (hγ : LipschitzOnWith C γ (Set.Icc a b)) :

eVariationOn γ (Set.Icc a b) = ENNReal.ofReal (∫ (x : ℝ) in a..b, ‖deriv γ x‖)

Total variation of a planar Lipschitz curve is the integral of its speed.

theorem MeasureTheory.hausdorffMeasure_image_Icc_eq_ofReal_integral_norm_deriv {γ : ℝ → EuclideanSpace ℝ (Fin 2)} {C : NNReal} {a b : ℝ} (hab : a ≤ b) (hγ : LipschitzOnWith C γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Icc a b)) :

(Measure.hausdorffMeasure 1) (γ '' Set.Icc a b) = ENNReal.ofReal (∫ (x : ℝ) in a..b, ‖deriv γ x‖)

Hausdorff length of a planar injective Lipschitz curve is the integral of its speed.

theorem MeasureTheory.volume_image_Icc_eq_zero_of_boundedVariationOn (γ : ℝ → EuclideanSpace ℝ (Fin 2)) {a b : ℝ} (hab : a ≤ b) (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Icc a b)) (hBV : BoundedVariationOn γ (Set.Icc a b)) :

volume (γ '' Set.Icc a b) = 0

The image of a continuous injective planar arc of bounded variation is Lebesgue null.

For Mathlib / Measure Theory / Hausdorff / Graph #

theorem MeasureTheory.map_firstCoordinate_restrict_curve_eq_withDensity {γ : ℝ → EuclideanSpace ℝ (Fin 2)} {C : NNReal} {a b : ℝ} (hab : a ≤ b) (hγ : LipschitzOnWith C γ (Set.Icc a b)) (hcoord : ∀ x ∈ Set.Icc a b, (γ x).ofLp 0 = x) :

Measure.map (fun (p : EuclideanSpace ℝ (Fin 2)) => p.ofLp 0) ((Measure.hausdorffMeasure 1).restrict (γ '' Set.Icc a b)) = (volume.restrict (Set.Icc a b)).withDensity fun (x : ℝ) => ENNReal.ofReal ‖deriv γ x‖

Projected Hausdorff measure on a Lipschitz graph has speed as its density.

theorem MeasureTheory.integral_restrict_curve_eq_integral_norm_deriv_mul {γ : ℝ → EuclideanSpace ℝ (Fin 2)} {C : NNReal} {a b : ℝ} (hab : a ≤ b) (hγ : LipschitzOnWith C γ (Set.Icc a b)) (hcoord : ∀ x ∈ Set.Icc a b, (γ x).ofLp 0 = x) {φ : EuclideanSpace ℝ (Fin 2) → ℝ} (hφ : Measurable φ) :

∫ (p : EuclideanSpace ℝ (Fin 2)) in γ '' Set.Icc a b, φ p ∂Measure.hausdorffMeasure 1 = ∫ (x : ℝ) in a..b, ‖deriv γ x‖ * φ (γ x)

Weighted arclength formula for a planar Lipschitz graph on a compact interval.

For Mathlib / Measure Theory / Hausdorff / Planar Graph #

theorem MeasureTheory.hausdorffMeasure_coordinateGraph_nondifferentiable_eq_zero {g : ℝ → ℝ} {a b : ℝ} (hg : LocallyLipschitzOn (Set.Ioo a b) g) (o : EuclideanSpace ℝ (Fin 2)) (e : EuclideanSpace ℝ (Fin 2) ≃ₗᵢ[ℝ ] EuclideanSpace ℝ (Fin 2)) :

(Measure.hausdorffMeasure 1) ((fun (x : ℝ) => o + e.symm !₂[x, g x]) '' {x : ℝ | x ∈ Set.Ioo a b ∧ ¬DifferentiableAt ℝ g x}) = 0

The graph image of the nondifferentiability set of a locally Lipschitz real function has zero one-dimensional Hausdorff measure, in isometric coordinates.

theorem MeasureTheory.integral_restrict_coordinateGraph_eq_integral_sqrt_mul {g : ℝ → ℝ} {C : NNReal} {a b : ℝ} (hab : a ≤ b) (hg : LipschitzOnWith C g (Set.Icc a b)) (o : EuclideanSpace ℝ (Fin 2)) (e : EuclideanSpace ℝ (Fin 2) ≃ₗᵢ[ℝ ] EuclideanSpace ℝ (Fin 2)) {φ : EuclideanSpace ℝ (Fin 2) → ℝ} (hφ : Measurable φ) :

∫ (p : EuclideanSpace ℝ (Fin 2)) in (fun (x : ℝ) => o + e.symm !₂[x, g x]) '' Set.Icc a b, φ p ∂Measure.hausdorffMeasure 1 = ∫ (x : ℝ) in a..b, √(1 + deriv g x ^ 2) * φ (o + e.symm !₂[x, g x])

Weighted Hausdorff integration over an isometric planar graph equals the parameter integral weighted by its almost-everywhere speed.

For Mathlib / Measure Theory / Integral / Atomic Bounds #

theorem MeasureTheory.sum_measureReal_mul_le_setIntegral {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) (D : Finset α) {E : Set α} {f : α → ℝ} (hE : MeasurableSet E) (hDE : ↑D ⊆ E) (hf : IntegrableOn f E μ) (hnonneg : ∀ x ∈ E, 0 ≤ f x) :

∑ x ∈ D, (μ {x}).toReal * f x ≤ ∫ (x : α) in E, f x ∂μ

A finite sum of atomic contributions is bounded by the integral of a nonnegative function.

For Mathlib / Measure Theory / Integral / Interval Exhaustion #

theorem MeasureTheory.eventually_mem_innerIcc_of_mem_Ioo {a b x : ℝ} (hx : x ∈ Set.Ioo a b) :

∀ᶠ (n : ℕ) in Filter.atTop , x ∈ Set.Icc (a + 1 / (↑n + 1)) (b - 1 / (↑n + 1))

Every interior point eventually belongs to the standard inner exhaustion of an interval.

theorem MeasureTheory.innerIcc_subset_Ioo (a b : ℝ) (n : ℕ) :

Set.Icc (a + 1 / (↑n + 1)) (b - 1 / (↑n + 1)) ⊆ Set.Ioo a b

Each interval in the standard inner exhaustion lies in the open interval.

theorem MeasureTheory.tendsto_integral_innerIcc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : Integrable f (volume.restrict (Set.Icc a b))) :

Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in Set.Icc (a + 1 / (↑n + 1)) (b - 1 / (↑n + 1)), f x) Filter.atTop (nhds (∫ (x : ℝ) in Set.Icc a b, f x))

Integrals over compact intervals exhausting the interior converge to the integral over the full compact interval.

For Mathlib / Measure Theory / Integral / Moving Intervals #

theorem MeasureTheory.ae_tendsto_indicator_Icc_of_tendsto_endpoints {E : Type u_1} [NormedAddCommGroup E] {a b : ℕ → ℝ} {c d : ℝ} {f : ℕ → ℝ → E} {g : ℝ → E} (ha : Filter.Tendsto a Filter.atTop (nhds c)) (hb : Filter.Tendsto b Filter.atTop (nhds d)) (hf : ∀ᵐ (x : ℝ), x ∈ Set.Ioo c d → Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) :

∀ᵐ (x : ℝ), Filter.Tendsto (fun (n : ℕ) => (Set.Icc (a n) (b n)).indicator (f n) x) Filter.atTop (nhds ((Set.Icc c d).indicator g x))

Moving interval cutoffs preserve almost-everywhere convergence on the limiting interior.

theorem MeasureTheory.tendsto_integral_Icc_of_tendsto_endpoints {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℕ → ℝ} {c d : ℝ} {f : ℕ → ℝ → E} {g : ℝ → E} {bound : ℝ → ℝ} (ha : Filter.Tendsto a Filter.atTop (nhds c)) (hb : Filter.Tendsto b Filter.atTop (nhds d)) (hmeas : ∀ᶠ (n : ℕ) in Filter.atTop , AEStronglyMeasurable (f n) (volume.restrict (Set.Icc (a n) (b n)))) (hbound : Integrable bound volume) (hbound_nonneg : ∀ᵐ (x : ℝ), 0 ≤ bound x) (hdom : ∀ᶠ (n : ℕ) in Filter.atTop , ∀ᵐ (x : ℝ), x ∈ Set.Icc (a n) (b n) → ‖f n x‖ ≤ bound x) (hf : ∀ᵐ (x : ℝ), x ∈ Set.Ioo c d → Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) :

Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in Set.Icc (a n) (b n), f n x) Filter.atTop (nhds (∫ (x : ℝ) in Set.Icc c d, g x))

Dominated convergence on intervals whose endpoints converge, using convergence only in the interior of the limiting interval.

theorem MeasureTheory.tendsto_integral_Icc_of_tendsto_endpoints_of_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℕ → ℝ} {c d M : ℝ} {f : ℕ → ℝ → E} {g : ℝ → E} (ha : Filter.Tendsto a Filter.atTop (nhds c)) (hb : Filter.Tendsto b Filter.atTop (nhds d)) (hmeas : ∀ᶠ (n : ℕ) in Filter.atTop , AEStronglyMeasurable (f n) (volume.restrict (Set.Icc (a n) (b n)))) (hM : 0 ≤ M) (hdom : ∀ᶠ (n : ℕ) in Filter.atTop , ∀ᵐ (x : ℝ), x ∈ Set.Icc (a n) (b n) → ‖f n x‖ ≤ M) (hf : ∀ᵐ (x : ℝ), x ∈ Set.Ioo c d → Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) :

Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in Set.Icc (a n) (b n), f n x) Filter.atTop (nhds (∫ (x : ℝ) in Set.Icc c d, g x))

A uniform bound on moving finite intervals suffices for dominated convergence.

For Mathlib / Measure Theory / Integral / Translation #

theorem MeasureTheory.integral_image_add_right_eq (c : ℝ) (E : Set ℝ) (hE : MeasurableSet E) (f : ℝ → ℝ) :

∫ (y : ℝ) in (fun (x : ℝ) => x + c) '' E, f y = ∫ (x : ℝ) in E, f (x + c)

Translation of a measurable real set preserves integrals.

theorem MeasureTheory.integral_Icc_const_add_eq (c a b : ℝ) (f : ℝ → ℝ) :

∫ (y : ℝ) in Set.Icc (c + a) (c + b), f y = ∫ (x : ℝ) in Set.Icc a b, f (x + c)

Translating both endpoints of a closed real interval translates the integrand.

theorem MeasureTheory.integrableOn_comp_add_right_iff (c : ℝ) (E : Set ℝ) (hE : MeasurableSet E) (f : ℝ → ℝ) :

IntegrableOn (fun (x : ℝ) => f (x + c)) E volume ↔ IntegrableOn f ((fun (x : ℝ) => x + c) '' E) volume

Integrability on a translated measurable set is preserved by translation.

theorem MeasureTheory.setLIntegral_comp_sub_right (w : ℝ → ENNReal) (c : ℝ) (A : Set ℝ) :

∫⁻ (u : ℝ) in A, w (u - c) = ∫⁻ (t : ℝ) in (fun (t : ℝ) => t + c) ⁻¹' A, w t

A lower Lebesgue integral of a right-translated function is the integral of the function itself over the translated set.

theorem MeasureTheory.map_add_right_restrict_withDensity (c : ℝ) (S : Set ℝ) (w : ℝ → ENNReal) :

Measure.map (fun (t : ℝ) => t + c) ((volume.restrict S).withDensity w) = (volume.restrict ((fun (t : ℝ) => t + c) '' S)).withDensity fun (u : ℝ) => w (u - c)

Pushing a weighted restriction of Lebesgue measure forward along t ↦ t + c translates both the set and the weight.

For Mathlib / Measure Theory / Measure / Atoms #

theorem MeasureTheory.ae_restrict_mem_of_countable_diff {α : Type u_1} [MeasurableSpace α] {μ : Measure α} [NullSingletonClass μ] {S A N : Set α} (hS : MeasurableSet S) (hN : N.Countable) (hsub : S \ A ⊆ N) :

∀ᵐ (x : α) ∂μ.restrict S, x ∈ A

A membership that fails only on a countable set holds almost everywhere on the restriction of a measure with null singletons.

theorem MeasureTheory.ae_measure_singleton_comp_eq_zero_of_injOn {X : Type u_1} [MeasurableSpace X] [MeasurableSingletonClass X] (μ : Measure X) [SFinite μ] {s : Set ℝ} (hs : MeasurableSet s) {f : ℝ → X} (hf : Set.InjOn f s) :

∀ᵐ (t : ℝ) ∂volume.restrict s, μ {f t} = 0

Along an injective parametrization, a finite-measure atom occurs only almost nowhere.

theorem MeasureTheory.measure_eq_sum_singleton_inter_of_compl_eq_zero {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) (S : Finset α) (hS : μ (↑S)ᶜ = 0) (E : Set α) (hE : MeasurableSet E) :

μ E = ∑ x ∈ S, μ ({x} ∩ E)

A measure carried by a finite set is the sum of its atomic contributions.

theorem MeasureTheory.measure_le_sum_of_measure_compl_image_eq_zero {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) (S S' : Finset ι) (f : ι → α) (b : ι → ENNReal) (hf : Set.InjOn f ↑S) (hS : μ (f '' ↑S)ᶜ = 0) (hb : ∀ i ∈ S, μ {f i} ≤ b i) (E : Set α) (hE : MeasurableSet E) (hactive : ∀ i ∈ S, f i ∈ E → i ∈ S') :

μ E ≤ ∑ i ∈ S', b i

A measure carried by the image of a finite index set is bounded by the sum of atomic bounds over any index subset containing every index whose atom meets the measured set.

Almost every point of a half-open interval is interior #

theorem MeasureTheory.ae_restrict_Ico_mem_Ioo {μ : Measure ℝ} [NullSingletonClass μ] (a b : ℝ) :

∀ᵐ (t : ℝ) ∂μ.restrict (Set.Ico a b), t ∈ Set.Ioo a b

Almost every point of a half-open interval, for a measure with null singletons, lies in the corresponding open interval.

theorem MeasureTheory.ae_restrict_Ioc_mem_Ioo {μ : Measure ℝ} [NullSingletonClass μ] (a b : ℝ) :

∀ᵐ (t : ℝ) ∂μ.restrict (Set.Ioc a b), t ∈ Set.Ioo a b

Almost every point of a half-open interval, for a measure with null singletons, lies in the corresponding open interval.

theorem MeasureTheory.ae_restrict_Ico_mem_Ioo_union_Ioo {μ : Measure ℝ} [NullSingletonClass μ] (a b c : ℝ) :

∀ᵐ (t : ℝ) ∂μ.restrict (Set.Ico a c), t ∈ Set.Ioo a b ∪ Set.Ioo b c

Almost every point of a half-open interval, for a measure with null singletons, lies in one of the two open intervals cut out by an arbitrary intermediate point.

theorem MeasureTheory.ae_restrict_Ioc_mem_Ioo_union_Ioo {μ : Measure ℝ} [NullSingletonClass μ] (a b c : ℝ) :

∀ᵐ (t : ℝ) ∂μ.restrict (Set.Ioc a c), t ∈ Set.Ioo a b ∪ Set.Ioo b c

Almost every point of a half-open interval, for a measure with null singletons, lies in one of the two open intervals cut out by an arbitrary intermediate point.

Haar-null lines and inner-product level sets #

Lines and hyperplanes of a finite-dimensional real normed space carry no additive Haar mass. This file records the two convenient forms used when a planar region is exhausted by triangles up to the rays through finitely many vertices.

theorem Submodule.span_singleton_ne_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 1 < Module.finrank ℝ E) (v : E) :

ℝ ∙ v ≠ ⊤

A line through the origin is a proper subspace once the ambient dimension exceeds one.

theorem MeasureTheory.Measure.addHaar_vadd_span_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E) [μ.IsAddHaarMeasure] (h : 1 < Module.finrank ℝ E) (o v : E) :

μ (o +ᵥ ↑(ℝ ∙ v)) = 0

Any line in a space of dimension at least two is null for an additive Haar measure.

theorem MeasureTheory.Measure.addHaar_iUnion_vadd_span_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {ι : Type u_2} [Countable ι] (μ : Measure E) [μ.IsAddHaarMeasure] (h : 1 < Module.finrank ℝ E) (o : E) (v : ι → E) :

μ (⋃ (i : ι), o +ᵥ ↑(ℝ ∙ v i)) = 0

A countable union of lines through a common point is null.

theorem MeasureTheory.Measure.addHaar_setOf_real_inner_eq {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] (μ : Measure F) [μ.IsAddHaarMeasure] {u : F} (hu : u ≠ 0) (c : ℝ) :

μ {p : F | inner ℝ p u = c} = 0

A level set of a nonzero inner-product functional is null for an additive Haar measure.

For Mathlib / Measure Theory / Measure / Map #

theorem MeasureTheory.Measure.map_map_of_ae_leftInverse {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {f : α → β} (hf : Measurable f) {g : β → α} (hg : Measurable g) (h : ∀ᵐ (a : α) ∂μ, g (f a) = a) :

map g (map f μ) = μ

If g is almost everywhere a left inverse of f, then pushing a measure forward along f and then along g recovers it. This is the almost-everywhere form of MeasurableEquiv.map_symm_map.

For Mathlib / Measure Theory / Measure / With Density #

theorem MeasureTheory.Measure.map_restrict_withDensity_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : Measure α) [NullSingletonClass μ] (f : α → β) (hf : Measurable f) (s : Set α) (hinj : Set.InjOn f s) (w : α → ENNReal) {x : α} (hx : x ∈ s) :

(map f ((μ.restrict s).withDensity w)) {f x} = 0

An injective image of a weighted restriction preserves null singleton masses.

theorem MeasureTheory.Measure.map_withDensity_eq_smul_add_smul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : Measure α) {φ : α → β} (hφ : Measurable φ) (a b : ENNReal) {w w₁ w₂ : α → ENNReal} (h₁ : Measurable w₁) (h₂ : Measurable w₂) (hw : ∀ (x : α), w x = a * w₁ x + b * w₂ x) :

map φ (μ.withDensity w) = a • map φ (μ.withDensity w₁) + b • map φ (μ.withDensity w₂)

Pushing a weighted measure forward along a measurable map is linear in the weight: if w is the pointwise combination a * w₁ + b * w₂, then the pushforward of μ.withDensity w is the same combination of the pushforwards of μ.withDensity w₁ and μ.withDensity w₂.

For Mathlib / Measure Theory / Region Between #

theorem volume_setOf_mem_Icc_eq_volume_regionBetween {f g : ℝ → ℝ} {s : Set ℝ} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :

MeasureTheory.volume {p : ℝ × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)} = MeasureTheory.volume (regionBetween f g s)

theorem volume_regionBetween_triangle {b h : ℝ} (hb : 0 < b) (hh : 0 ≤ h) :

MeasureTheory.volume (regionBetween (fun (x : ℝ) => 0) (fun (x : ℝ) => h - h / b * x) (Set.Ioc 0 b)) = ENNReal.ofReal (b * h / 2)

theorem volume_setOf_mem_Ioc_eq_volume_regionBetween {f g : ℝ → ℝ} {s : Set ℝ} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) :

MeasureTheory.volume {p : ℝ × ℝ | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)} = MeasureTheory.volume (regionBetween f g s)

theorem volume_horizontalIcc {f g : ℝ → ℝ} {s : Set ℝ} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) (hfi : MeasureTheory.IntegrableOn f s MeasureTheory.volume) (hgi : MeasureTheory.IntegrableOn g s MeasureTheory.volume) (hfg : ∀ x ∈ s, f x ≤ g x) :

MeasureTheory.volume {p : EuclideanSpace ℝ (Fin 2) | p.ofLp 1 ∈ s ∧ p.ofLp 0 ∈ Set.Icc (f (p.ofLp 1)) (g (p.ofLp 1))} = ENNReal.ofReal (∫ (x : ℝ) in s, (g - f) x)

The planar volume of the horizontal band between the graphs of f and g over s, where the first coordinate is the one squeezed between the two graphs.

theorem volume_horizontalIoc {f g : ℝ → ℝ} {s : Set ℝ} (hf : Measurable f) (hg : Measurable g) (hs : MeasurableSet s) (hfi : MeasureTheory.IntegrableOn f s MeasureTheory.volume) (hgi : MeasureTheory.IntegrableOn g s MeasureTheory.volume) (hfg : ∀ x ∈ s, f x ≤ g x) :

MeasureTheory.volume {p : EuclideanSpace ℝ (Fin 2) | p.ofLp 1 ∈ s ∧ p.ofLp 0 ∈ Set.Ioc (f (p.ofLp 1)) (g (p.ofLp 1))} = ENNReal.ofReal (∫ (x : ℝ) in s, (g - f) x)

The half-open variant of volume_horizontalIcc.

theorem volume_le_of_subset_horizontalBand {X : Set (EuclideanSpace ℝ (Fin 2))} {f : ℝ → ℝ} {c : ℝ} (hf : Continuous f) (hc : 0 ≤ c) (hX : ∀ p ∈ X, (0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1) ∧ f (p.ofLp 1) ≤ p.ofLp 0 ∧ p.ofLp 0 ≤ f (p.ofLp 1) + c) :

MeasureTheory.volume X ≤ ENNReal.ofReal c

A planar set whose second coordinate lies in [0, 1] and whose first coordinate is squeezed between a continuous graph and its horizontal translate by c has volume at most c. Only the upper bound is asserted, so no measurability of the set is needed.

theorem volume_horizontalBand_inter_le (a b c : ℝ) (ha : a ≠ 0) :

MeasureTheory.volume {p : EuclideanSpace ℝ (Fin 2) | (0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1) ∧ c ≤ a * p.ofLp 0 + b * p.ofLp 1 ∧ a * p.ofLp 0 + b * p.ofLp 1 ≤ c + 1} ≤ ENNReal.ofReal (1 / |a|)

The horizontal unit strip meets the band c ≤ a * x + b * y ≤ c + 1 in a parallelogram of area 1 / |a|. Only the upper bound is asserted.

Planar trapezoids with horizontal parallel sides #

theorem EuclideanSpace.horizontalTrapezoid_subset_of_convex {S : Set (EuclideanSpace ℝ (Fin 2))} (hS : Convex ℝ S) {l₀ r₀ l₁ r₁ : ℝ} (h₀l : !₂[l₀, 0] ∈ S) (h₀r : !₂[r₀, 0] ∈ S) (h₁l : !₂[l₁, 1] ∈ S) (h₁r : !₂[r₁, 1] ∈ S) :

{q : EuclideanSpace ℝ (Fin 2) | q.ofLp 1 ∈ Set.Icc 0 1 ∧ q.ofLp 0 ∈ Set.Icc ((1 - q.ofLp 1) * l₀ + q.ofLp 1 * l₁) ((1 - q.ofLp 1) * r₀ + q.ofLp 1 * r₁)} ⊆ S

A convex planar set containing the four vertices of a trapezoid whose parallel sides are the horizontal segments at heights 0 and 1 contains the whole trapezoid.

theorem EuclideanSpace.volume_horizontalTrapezoid_band {y₀ y₁ a b c d : ℝ} (hy : y₀ ≤ y₁) (h₀ : a + b * y₀ ≤ c + d * y₀) (h₁ : a + b * y₁ ≤ c + d * y₁) :

MeasureTheory.volume {q : EuclideanSpace ℝ (Fin 2) | q.ofLp 1 ∈ Set.Icc y₀ y₁ ∧ q.ofLp 0 ∈ Set.Icc (a + b * q.ofLp 1) (c + d * q.ofLp 1)} = ENNReal.ofReal ((y₁ - y₀) * (c + d * y₀ - (a + b * y₀) + (c + d * y₁ - (a + b * y₁))) / 2)

The planar area of the trapezoid cut from the horizontal band y₀ ≤ y ≤ y₁ by the two lines x = a + b * y and x = c + d * y: the height of the band times the mean of the lengths of its two horizontal sides.

theorem EuclideanSpace.volume_horizontalTrapezoid {l₀ r₀ l₁ r₁ : ℝ} (h₀ : l₀ ≤ r₀) (h₁ : l₁ ≤ r₁) :

MeasureTheory.volume {q : EuclideanSpace ℝ (Fin 2) | q.ofLp 1 ∈ Set.Icc 0 1 ∧ q.ofLp 0 ∈ Set.Icc ((1 - q.ofLp 1) * l₀ + q.ofLp 1 * l₁) ((1 - q.ofLp 1) * r₀ + q.ofLp 1 * r₁)} = ENNReal.ofReal ((r₀ - l₀ + (r₁ - l₁)) / 2)

The planar area of a trapezoid whose parallel sides are the horizontal segments [l₀, r₀] × {0} and [l₁, r₁] × {1} is the mean of their lengths.

The area of a planar triangle #

The convex hull of three points of the Euclidean plane has area one half of the absolute determinant of the two edge vectors emanating from the first point. The proof transports the standard right triangle, whose area is computed by integration, along the linear map sending the coordinate basis to the two edge vectors.

theorem EuclideanSpace.volume_convexHull_zero_pair (u v : EuclideanSpace ℝ (Fin 2)) :

MeasureTheory.volume ((convexHull ℝ) {0, u, v}) = ENNReal.ofReal (|u.ofLp 0 * v.ofLp 1 - v.ofLp 0 * u.ofLp 1| / 2)

The triangle spanned by the origin and two vectors of the Euclidean plane has area one half of the absolute determinant of their coordinates.

theorem EuclideanSpace.volume_convexHull_triple (a b c : EuclideanSpace ℝ (Fin 2)) :

MeasureTheory.volume ((convexHull ℝ) {a, b, c}) = ENNReal.ofReal (|(b - a).ofLp 0 * (c - a).ofLp 1 - (c - a).ofLp 0 * (b - a).ofLp 1| / 2)

The area of a planar triangle is one half of the absolute coordinate determinant of its two edge vectors.

For Mathlib / Measure Theory / Stieltjes Density #

theorem BoundedVariationOn.vectorMeasure_eq_withDensity_of_integral_Icc {α : Type u_1} {E : Type u_2} [LinearOrder α] [DenselyOrdered α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [CompactIccSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f r : α → E} {μ : MeasureTheory.Measure α} (hf : BoundedVariationOn f Set.univ) (hcont : Continuous f) (hr : MeasureTheory.Integrable r μ) (hinc : ∀ (a b : α), a ≤ b → f b - f a = ∫ (x : α) in Set.Icc a b, r x ∂μ) :

hf.vectorMeasure = μ.withDensityᵥ r

Equality of interval increments identifies a continuous BV function's vector measure.

theorem MeasureTheory.integral_subtype_preimage {α : Type u_1} {E : Type u_2} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (f : α → E) :

∫ (x : { x : α // x ∈ s }) in {x : ↑s | ↑x ∈ t}, f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α) in t, f x ∂μ.restrict s

Integrating on a subtype and a measurable preimage agrees with restricting both sets.

For Mathlib / Measure Theory / Vector Measure / Interval #

theorem MeasureTheory.VectorMeasure.ext_of_Ioc {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] (μ ν : VectorMeasure α E) (h : ∀ (a b : α), a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)) (huniv : μ Set.univ = ν Set.univ) :

μ = ν

Agreement on half-open intervals and the whole space determines a vector measure.

theorem MeasurableEmbedding.exists_vectorMeasure_image_integral {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → β} (hf : MeasurableEmbedding f) (μ : MeasureTheory.Measure β) (g : β → E) (hg : MeasureTheory.Integrable g μ) :

∃ (ν : MeasureTheory.VectorMeasure α E), ∀ (s : Set α), MeasurableSet s → ν s = ∫ (x : β) in f '' s, g x ∂μ

Pulling an integrable density back along a measurable embedding gives its image integrals.

For Mathlib / Measure Theory / Vector Measure / With Density #

theorem MeasureTheory.VectorMeasure.setIntegral_withDensity_mul_of_bounded {X : Type u_1} [MeasurableSpace X] {μ : Measure X} {r q : X → ℝ} (hr : Integrable r μ) (hq : AEStronglyMeasurable q μ) (C : ℝ) (hq_bound : ∀ (x : X), ‖q x‖ ≤ C) (E : Set X) (hE : MeasurableSet E) :

∫ᵛ (x : X) in E, q x ∂[ContinuousLinearMap.mul ℝ ℝ; μ.withDensityᵥ r] = ∫ (x : X) in E, q x * r x ∂μ

Integrating a bounded function against a real signed density multiplies the ordinary integrand by that density.

theorem MeasureTheory.VectorMeasure.setIntegral_withDensity_mul {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [BorelSpace X] [CompactSpace X] {μ : Measure X} {r q : X → ℝ} (hr : Integrable r μ) (hq : Continuous q) (E : Set X) (hE : MeasurableSet E) :

∫ᵛ (x : X) in E, q x ∂[ContinuousLinearMap.mul ℝ ℝ; μ.withDensityᵥ r] = ∫ (x : X) in E, q x * r x ∂μ

Integrating a continuous real function on a compact space against a signed density multiplies the ordinary integrand by that density.

For Mathlib / Measure Theory / Volume #

theorem MeasureTheory.volume_smul_rpow_half (S : Set (EuclideanSpace ℝ (Fin 2))) (a : ℝ) (ha : 0 ≤ a) :

volume (a • S) ^ 2⁻¹ = ENNReal.ofReal a * volume S ^ 2⁻¹

The square root of planar volume scales linearly under nonnegative dilations.

ForMathlib.Order.Infimum.
ForMathlib.Order.IntervalPartition.

For Mathlib / Order / Infimum #

theorem abs_sInf_image_sub_sInf_image_le {ι : Type u_1} {s : Set ι} (hs : s.Nonempty) (f g : ι → ℝ) (hf : BddBelow (f '' s)) (hg : BddBelow (g '' s)) {C : ℝ} (h : ∀ x ∈ s, |f x - g x| ≤ C) :

|sInf (f '' s) - sInf (g '' s)| ≤ C

Uniformly close real functions have uniformly close infima on a nonempty set.

For Mathlib / Order / Interval Partition #

theorem Monotone.iUnion_Ioc_fin {α : Type u_1} [LinearOrder α] {n : ℕ} (cuts : Fin (n + 1) → α) (hcuts : Monotone cuts) :

⋃ (i : Fin n), Set.Ioc (cuts i.castSucc) (cuts i.succ) = Set.Ioc (cuts 0) (cuts (Fin.last n))

Adjacent half-open intervals of a finite monotone sequence cover its endpoint interval.

ForMathlib.Topology.Angle.
ForMathlib.Topology.Order.Compact.
ForMathlib.Topology.Order.Concatenation.
ForMathlib.Topology.Order.Interval.
ForMathlib.Topology.Order.IntervalExtension.

For Mathlib / Topology / Angle #

theorem Real.Angle.exists_continuous_lift_zero (θ : ↑unitInterval → Angle) (hθ : Continuous θ) (hzero : θ 0 = 0) :

∃ (α : ↑unitInterval → ℝ), Continuous α ∧ α 0 = 0 ∧ ∀ (t : ↑unitInterval), ↑(α t) = θ t

A continuous angle path starting at zero has a continuous real lift starting at zero.

For Mathlib / Topology / Order / Compact #

theorem IsCompact.exists_pos_forall_le {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hne : s.Nonempty) {f : X → ℝ} (hf : ContinuousOn f s) (hpos : ∀ x ∈ s, 0 < f x) :

∃ m > 0, ∀ x ∈ s, m ≤ f x

A positive continuous function has a positive uniform lower bound on a nonempty compact set.

For Mathlib / Topology / Order / Concatenation #

noncomputable def Function.concatUnitIntervals {E : Type u_1} (x y : ↑(Set.Icc 0 1) → E) (t : ↑(Set.Icc 0 2)) :

Concatenate two functions on [0, 1] on the interval [0, 2].

Equations

Function.concatUnitIntervals x y t = if ↑t ≤ 1 then x (Set.projIcc 0 1 Function.concatUnitIntervals._proof_1 ↑t) else y (Set.projIcc 0 1 Function.concatUnitIntervals._proof_1 (↑t - 1))

Instances For

theorem Function.continuous_concatUnitIntervals {E : Type u_1} [TopologicalSpace E] {x y : ↑(Set.Icc 0 1) → E} (hx : Continuous x) (hy : Continuous y) (hjoin : x ⟨1, continuous_concatUnitIntervals._proof_1 ⟩ = y ⟨0, continuous_concatUnitIntervals._proof_2 ⟩) :

Continuous (concatUnitIntervals x y)

Concatenation is continuous when the endpoint values agree.

@[simp]

theorem Function.concatUnitIntervals_zero {E : Type u_1} (x y : ↑(Set.Icc 0 1) → E) :

concatUnitIntervals x y ⟨0, concatUnitIntervals_zero._proof_1 ⟩ = x ⟨0, continuous_concatUnitIntervals._proof_2 ⟩

@[simp]

theorem Function.concatUnitIntervals_one {E : Type u_1} (x y : ↑(Set.Icc 0 1) → E) :

concatUnitIntervals x y ⟨1, concatUnitIntervals_one._proof_1 ⟩ = x ⟨1, continuous_concatUnitIntervals._proof_1 ⟩

@[simp]

theorem Function.concatUnitIntervals_two {E : Type u_1} (x y : ↑(Set.Icc 0 1) → E) :

concatUnitIntervals x y ⟨2, concatUnitIntervals_two._proof_1 ⟩ = y ⟨1, continuous_concatUnitIntervals._proof_1 ⟩

theorem Function.range_concatUnitIntervals {E : Type u_1} (x y : ↑(Set.Icc 0 1) → E) (hjoin : x ⟨1, continuous_concatUnitIntervals._proof_1 ⟩ = y ⟨0, continuous_concatUnitIntervals._proof_2 ⟩) :

Set.range (concatUnitIntervals x y) = Set.range x ∪ Set.range y

Joined paths have precisely the union of the two original ranges.

theorem Function.injOn_concatUnitIntervals_comp_of_cyclic_endpoints {E : Type u_1} {a b : ℝ} (hab : a ≤ b) {x : ↑(Set.Icc a b) → E} (hinj : Set.InjOn x {t : ↑(Set.Icc a b) | ↑t < b}) (hclosed : x ⟨a, ⋯⟩ = x ⟨b, ⋯⟩) (s : ↑(Set.Icc a b)) (has : a < ↑s) (hsb : ↑s < b) (φ ψ : ↑(Set.Icc 0 1) → ↑(Set.Icc a b)) (hφ : StrictMono φ) (hψ : StrictMono ψ) (hφ₀ : φ ⟨0, continuous_concatUnitIntervals._proof_2 ⟩ = s) (hψ₀ : ψ ⟨0, continuous_concatUnitIntervals._proof_2 ⟩ = ⟨a, ⋯⟩) (hψ₁ : ψ ⟨1, continuous_concatUnitIntervals._proof_1 ⟩ = s) :

Set.InjOn (concatUnitIntervals (x ∘ φ) (x ∘ ψ)) {t : ↑(Set.Icc 0 2) | ↑t < 2}

A strict cyclic cut preserves injectivity away from the final endpoint.

For Mathlib / Topology / Order / Interval #

instance Set.instCompactIccSpaceIcc (a b : ℝ) :

CompactIccSpace ↑(Icc a b)

def Set.Icc.reverse {a b : ℝ} (_hab : a ≤ b) :

↑(Icc a b) → ↑(Icc a b)

Reverse a closed real interval about its midpoint.

Equations

Set.Icc.reverse _hab t = ⟨a + b - ↑t, ⋯⟩

Instances For

theorem Set.Icc.continuous_reverse {a b : ℝ} (hab : a ≤ b) :

Continuous (reverse hab)

Interval reversal is continuous.

theorem Set.Icc.antitone_reverse {a b : ℝ} (hab : a ≤ b) :

Antitone (reverse hab)

Interval reversal is antitone.

theorem Set.Icc.involutive_reverse {a b : ℝ} (hab : a ≤ b) :

Function.Involutive (reverse hab)

Reversing a closed interval twice is the identity.

theorem Set.Icc.surjective_reverse {a b : ℝ} (hab : a ≤ b) :

Function.Surjective (reverse hab)

Interval reversal is surjective.

theorem continuousOn_replace_right_endpoint {E : Type u_1} [TopologicalSpace E] {a b : ℝ} (hab : a < b) (f : ℝ → E) (z : E) (hr : ∀ t ∈ Set.Ico a b, Filter.Tendsto f (nhdsWithin t (Set.Ioi t)) (nhds (f t))) (hl : ∀ t ∈ Set.Ioo a b, Filter.Tendsto f (nhdsWithin t (Set.Iio t)) (nhds (f t))) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds z)) :

ContinuousOn (fun (t : ℝ) => if t = b then z else f t) (Set.Icc a b)

Replace the terminal value of a one-sided continuous function by its left limit.

theorem Set.Icc.exists_partitions_mesh_tendsto_zero {a b : ℝ} (hab : a ≤ b) :

∃ (cuts : (k : ℕ) → Fin (k + 2) → ↑(Icc a b)), (∀ (k : ℕ), Monotone (cuts k)) ∧ (∀ (k : ℕ), ↑(cuts k 0) = a) ∧ (∀ (k : ℕ), ↑(cuts k (Fin.last (k + 1))) = b) ∧ ∀ δ > 0, ∀ᶠ (k : ℕ) in Filter.atTop , ∀ (i : Fin (k + 1)), ↑(cuts k i.succ) - ↑(cuts k i.castSucc) < δ

Every compact real interval carries finite monotone partitions, with prescribed endpoints, whose mesh eventually falls below any positive threshold.

theorem Set.Icc.exists_affine_monotone_surjection {a b c d : ℝ} (hab : a < b) (hcd : c < d) :

∃ (φ : ↑(Icc a b) → ↑(Icc c d)), Continuous φ ∧ Monotone φ ∧ Function.Surjective φ ∧ ∀ (t : ↑(Icc a b)), ↑(φ t) = c + (↑t - a) / (b - a) * (d - c)

The increasing affine surjection between two nondegenerate closed intervals.

theorem Set.Icc.exists_affine_antitone_surjection {a b c d : ℝ} (hab : a < b) (hcd : c < d) :

∃ (φ : ↑(Icc a b) → ↑(Icc c d)), Continuous φ ∧ Antitone φ ∧ Function.Surjective φ ∧ ∀ (t : ↑(Icc a b)), ↑(φ t) = d - (↑t - a) / (b - a) * (d - c)

The decreasing affine surjection between two nondegenerate closed intervals: the increasing one reflected in the midpoint of its codomain.

theorem Set.Icc.exists_translation_surjection {c d : ℝ} (hcd : d = c + 1) :

∃ (φ : ↑(Icc 0 1) → ↑(Icc c d)), Continuous φ ∧ Monotone φ ∧ Function.Surjective φ ∧ ∀ (u : ↑(Icc 0 1)), ↑(φ u) = c + ↑u

The translation of the unit interval onto a closed interval of length one.

For Mathlib / Topology / Order / Interval Extension #

noncomputable def OrderIso.extendIoo {a b c d : ℝ} (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) (x : ↑(Set.Icc a b)) :

↑(Set.Icc c d)

Extend an order isomorphism of open real intervals by matching the endpoints.

Equations

OrderIso.extendIoo hcd e x = if hxa : ↑x = a then ⟨c, ⋯⟩ else if hxb : ↑x = b then ⟨d, ⋯⟩ else let t := e ⟨↑x, ⋯⟩; ⟨↑t, ⋯⟩

Instances For

theorem OrderIso.extendIoo_left {a b c d : ℝ} (hab : a < b) (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) :

extendIoo hcd e ⟨a, ⋯⟩ = ⟨c, ⋯⟩

The extension maps the left endpoint to the left endpoint.

theorem OrderIso.extendIoo_right {a b c d : ℝ} (hab : a < b) (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) :

extendIoo hcd e ⟨b, ⋯⟩ = ⟨d, ⋯⟩

The extension maps the right endpoint to the right endpoint.

theorem OrderIso.extendIoo_interior {a b c d : ℝ} (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) (x : ↑(Set.Ioo a b)) :

↑(extendIoo hcd e ⟨↑x, ⋯⟩) = ↑(e x)

The extension agrees with the original order isomorphism on the interior.

theorem OrderIso.monotone_extendIoo {a b c d : ℝ} (hab : a < b) (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) :

Monotone (extendIoo hcd e)

The endpoint extension is monotone.

theorem OrderIso.surjective_extendIoo {a b c d : ℝ} (hab : a < b) (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) :

Function.Surjective (extendIoo hcd e)

The endpoint extension is surjective.

theorem OrderIso.continuous_extendIoo {a b c d : ℝ} (hab : a < b) (hcd : c < d) (e : ↑(Set.Ioo a b) ≃o ↑(Set.Ioo c d)) :

Continuous (extendIoo hcd e)

The endpoint extension is continuous.

ForMathlib.MeasureTheory.StieltjesTransport.
ForMathlib.MeasureTheory.VectorMeasure.LocallyConstant.

For Mathlib / Measure Theory / Stieltjes Transport #

theorem BoundedVariationOn.comp_monotone_surjective_Icc {a b c d : ℝ} (_hab : a ≤ b) {f : ↑(Set.Icc a b) → ℝ} (hf : BoundedVariationOn f Set.univ) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφ : Monotone φ) (hφs : Function.Surjective φ) :

BoundedVariationOn (f ∘ φ) Set.univ

A monotone surjection of compact intervals preserves bounded variation.

theorem BoundedVariationOn.vectorMeasure_map_comp_monotone_surjective_Icc {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) {f : ↑(Set.Icc a b) → ℝ} (hf : BoundedVariationOn f Set.univ) (hfc : Continuous f) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφc : Continuous φ) (hφ : Monotone φ) (hφs : Function.Surjective φ) :

⋯.vectorMeasure.map φ = hf.vectorMeasure

The Stieltjes measure is preserved by continuous monotone surjective reparametrization.

theorem BoundedVariationOn.vectorMeasure_singleton_eq_zero_of_continuous {a b : ℝ} {f : ↑(Set.Icc a b) → ℝ} (hf : BoundedVariationOn f Set.univ) (hfc : Continuous f) (x : ↑(Set.Icc a b)) :

hf.vectorMeasure {x} = 0

The Stieltjes measure of a continuous BV function has no point masses.

theorem BoundedVariationOn.vectorMeasure_map_Icc_inclusion {a b : ℝ} {f : ↑(Set.Icc a b) → ℝ} (hf : BoundedVariationOn f Set.univ) (hfc : Continuous f) (l u : ↑(Set.Icc a b)) (hlu : l ≤ u) :

let ι := fun (x : ↑(Set.Icc ↑l ↑u)) => ⟨↑x, ⋯⟩; have hfr := ⋯; hfr.vectorMeasure.map ι = hf.vectorMeasure.restrict (Set.Ioc l u)

The Stieltjes measure on a closed subinterval pushes forward to the half-open restriction.

theorem BoundedVariationOn.comp_antitone_surjective_Icc {a b c d : ℝ} (_hab : a ≤ b) {f : ↑(Set.Icc a b) → ℝ} (hf : BoundedVariationOn f Set.univ) {φ : ↑(Set.Icc c d) → ↑(Set.Icc a b)} (hφ : Antitone φ) (hφs : Function.Surjective φ) :

BoundedVariationOn (f ∘ φ) Set.univ

An antitone surjection of compact intervals preserves bounded variation.

theorem BoundedVariationOn.vectorMeasure_map_reverse_Icc {a b : ℝ} (hab : a ≤ b) {f : ↑(Set.Icc a b) → ℝ} (hf : BoundedVariationOn f Set.univ) (hfc : Continuous f) :

have r := Set.Icc.reverse hab; have hfr := ⋯; hfr.vectorMeasure.map r = -hf.vectorMeasure

Reversing a continuous BV function negates its transported Stieltjes measure.

For Mathlib / Measure Theory / Vector Measure / Locally Constant #

theorem BoundedVariationOn.exists_nhds_variation_vectorMeasure_eq_zero_of_eventuallyEq_const {a b : ℝ} (hab : a < b) {g : ↑(Set.Icc a b) → ℝ} (hg : BoundedVariationOn g Set.univ) (hr : ∀ (y : ↑(Set.Icc a b)), ContinuousWithinAt g (Set.Ici y) y) (x : ↑(Set.Icc a b)) (hxbot : a < ↑x) (hx : g =ᶠ[nhds x] fun (x_1 : ↑(Set.Icc a b)) => g x) :

∃ U ∈ nhds x, hg.vectorMeasure.variation U = 0

Local constancy away from the initial endpoint gives a variation-null neighborhood.

Geometry.Foundations.Development001.
Cap.Foundations.Development001.
Polygon.Foundations.Development001.

Geometry.Plane.
Geometry.Basic.
Geometry.Frame.
Geometry.NormalLines.
Geometry.QuadrantBounds.
Geometry.Subgraph.
Geometry.Support.
Geometry.Contacts.
Geometry.FrameCalculus.

Geometry / Plane #

@[reducible, inline]

abbrev MovingSofa.Point :

The two-dimensional real Euclidean space used for sofa geometry.

Equations

MovingSofa.Point = EuclideanSpace ℝ (Fin 2)

Instances For

theorem MovingSofa.Point.norm_sq_eq (z : Point) :

‖z‖ ^ 2 = z.ofLp 0 ^ 2 + z.ofLp 1 ^ 2

The squared norm of a planar point in coordinates.

theorem MovingSofa.Point.abs_inner_coords_le (w d : Point) :

|w.ofLp 0 * d.ofLp 0 + w.ofLp 1 * d.ofLp 1| ≤ ‖w‖ * ‖d‖

Cauchy-Schwarz for the coordinate form of the planar inner product.

theorem MovingSofa.Point.abs_apply_le_norm (z : Point) (i : Fin 2) :

|z.ofLp i| ≤ ‖z‖

Each coordinate of a planar point is bounded by its norm.

Geometry / Basic #

noncomputable def MovingSofa.frame (t : Real.Angle) :

Point × Point

The normal and positively oriented tangent at an angular direction.

Equations

MovingSofa.frame t = (!₂[t.cos, t.sin], !₂[-t.sin, t.cos])

Instances For

@[reducible, inline]

noncomputable abbrev MovingSofa.normalVector (t : Real.Angle) :

Point

The unit normal of the angular frame.

Equations

MovingSofa.normalVector t = (MovingSofa.frame t).1

Instances For

@[reducible, inline]

noncomputable abbrev MovingSofa.tangentVector (t : Real.Angle) :

Point

The counterclockwise unit tangent of the angular frame.

Equations

MovingSofa.tangentVector t = (MovingSofa.frame t).2

Instances For

noncomputable def MovingSofa.supportValue (s : Set Point) (t : Real.Angle) :

The support value; geometric results require a nonempty compact set.

Equations

MovingSofa.supportValue s t = sSup ((fun (p : MovingSofa.Point) => inner ℝ p (MovingSofa.normalVector t)) '' s)

Instances For

def MovingSofa.normalLine (t : Real.Angle) (h : ℝ) :

The line with the given unit normal and signed offset.

Equations

MovingSofa.normalLine t h = {p : MovingSofa.Point | inner ℝ p (MovingSofa.normalVector t) = h}

Instances For

def MovingSofa.normalHalfPlane (t : Real.Angle) (h : ℝ) (upper strict : Bool) :

A normal half-plane: upper chooses the greater side, strict its open version.

Equations

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

Instances For

theorem MovingSofa.isClosed_normalHalfPlane (t : Real.Angle) (h : ℝ) (upper : Bool) :

IsClosed (normalHalfPlane t h upper false)

Closed normal half-planes are closed, on either side of the boundary line.

theorem MovingSofa.convex_normalHalfPlane (t : Real.Angle) (h : ℝ) (upper : Bool) :

Convex ℝ (normalHalfPlane t h upper false)

Closed normal half-planes are convex, on either side of the boundary line.

theorem MovingSofa.convex_normalHalfPlane_open (t : Real.Angle) (h : ℝ) (upper : Bool) :

Convex ℝ (normalHalfPlane t h upper true)

Open normal half-planes are convex, on either side of the boundary line.

def MovingSofa.supportingLineHalfPlane (s : Set Point) (t : Real.Angle) :

Set Point × Set Point

The supporting line and closed containing half-plane of a nonempty compact set.

Equations

MovingSofa.supportingLineHalfPlane s t = (MovingSofa.normalLine t (MovingSofa.supportValue s t), MovingSofa.normalHalfPlane t (MovingSofa.supportValue s t) false false)

Instances For

theorem MovingSofa.supportingLineHalfPlane_snd_eq_normalHalfPlane {s : Set Point} {t u : Real.Angle} {h : ℝ} (hn : normalVector u = -normalVector t) (hs : supportValue s u = -h) :

(supportingLineHalfPlane s u).2 = normalHalfPlane t h true false

A closed supporting half-plane, read through the opposite normal direction.

Geometry / Frame #

theorem MovingSofa.exists_angle_normalVector_eq {u : Point} (hu : ‖u‖ = 1) :

∃ (t : Real.Angle), normalVector t = u

Every unit vector is the normal vector of an angular frame.

theorem MovingSofa.continuous_normalVector_real :

Continuous fun (t : ℝ) => normalVector ↑t

theorem MovingSofa.normalVector_add_pi (t : ℝ) :

normalVector ↑(t + Real.pi) = -normalVector ↑t

Opposite real angles give opposite normal vectors.

theorem MovingSofa.tangentVector_add_pi (t : ℝ) :

tangentVector ↑(t + Real.pi) = -tangentVector ↑t

Opposite real angles give opposite tangent vectors.

theorem MovingSofa.inner_normalVector_real (p : Point) (t : ℝ) :

inner ℝ p (normalVector ↑t) = p.ofLp 0 * Real.cos t + p.ofLp 1 * Real.sin t

The projection onto the normal direction of a real angle, in coordinates.

theorem MovingSofa.inner_tangentVector_real (p : Point) (t : ℝ) :

inner ℝ p (tangentVector ↑t) = -(p.ofLp 0 * Real.sin t) + p.ofLp 1 * Real.cos t

The projection onto the tangent direction of a real angle, in coordinates.

theorem MovingSofa.inner_normalVector_normalVector (s t : ℝ) :

inner ℝ (normalVector ↑s) (normalVector ↑t) = Real.cos (s - t)

The inner product of two unit normals is the cosine of their angle difference.

theorem MovingSofa.inner_normalVector_self (t : ℝ) :

inner ℝ (normalVector ↑t) (normalVector ↑t) = 1

A normal vector has squared length one.

theorem MovingSofa.inner_normalVector_self_angle (t : Real.Angle) :

inner ℝ (normalVector t) (normalVector t) = 1

A normal vector at an angle has squared length one.

theorem MovingSofa.norm_normalVector_real (t : ℝ) :

‖normalVector ↑t‖ = 1

A normal vector at a real angle has length one.

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

inner ℝ p (normalVector t) • normalVector t + inner ℝ p (tangentVector t) • tangentVector t = p

theorem MovingSofa.normalVector_add_real (t δ : ℝ) :

normalVector ↑(t + δ) = Real.cos δ • normalVector ↑t + Real.sin δ • tangentVector ↑t

theorem MovingSofa.inner_normalVector_tangentVector (t : ℝ) :

inner ℝ (normalVector ↑t) (tangentVector ↑t) = 0

theorem MovingSofa.inner_tangentVector_self (t : ℝ) :

inner ℝ (tangentVector ↑t) (tangentVector ↑t) = 1

theorem MovingSofa.tangentVector_add_pi_div_two (t : ℝ) :

tangentVector ↑(t + Real.pi / 2) = -normalVector ↑t

theorem MovingSofa.normalVector_add_pi_angle (a : Real.Angle) :

normalVector (a + ↑Real.pi) = -normalVector a

Adding pi to an angle reverses its normal vector.

theorem MovingSofa.sin_sub_eq_neg_inner_normalVector_tangentVector (t u : Real.Angle) :

(u - t).sin = -inner ℝ (normalVector t) (tangentVector u)

The sine convolution kernel is the negative normal projection of the moving tangent.

theorem MovingSofa.inner_tangentVector_normalVector_real (t s : ℝ) :

inner ℝ (tangentVector ↑t) (normalVector ↑s) = Real.sin (s - t)

The normal projection of a tangent vector is the sine of the angle difference.

theorem MovingSofa.inner_tangentVector_tangentVector (s t : ℝ) :

inner ℝ (tangentVector ↑s) (tangentVector ↑t) = Real.cos (s - t)

The inner product of two unit tangents is the cosine of their angle difference.

theorem MovingSofa.inner_normalVector_eq_frame_rotate (w : Point) (s t : ℝ) :

inner ℝ w (normalVector ↑t) = inner ℝ w (normalVector ↑s) * Real.cos (s - t) - inner ℝ w (tangentVector ↑s) * Real.sin (s - t)

The normal coordinate of a vector in the frame at another angle.

theorem MovingSofa.inner_tangentVector_eq_frame_rotate (w : Point) (s t : ℝ) :

inner ℝ w (tangentVector ↑t) = inner ℝ w (normalVector ↑s) * Real.sin (s - t) + inner ℝ w (tangentVector ↑s) * Real.cos (s - t)

The tangent coordinate of a vector in the frame at another angle.

theorem MovingSofa.eq_of_inner_normalVector_eq {p q : Point} {s t : ℝ} (hst : Real.sin (s - t) ≠ 0) (hs : inner ℝ p (normalVector ↑s) = inner ℝ q (normalVector ↑s)) (ht : inner ℝ p (normalVector ↑t) = inner ℝ q (normalVector ↑t)) :

p = q

Two points whose normal coordinates agree at two transverse angles coincide.

theorem MovingSofa.continuous_tangentVector_coordinate (i : Fin 2) :

Continuous fun (u : Real.Angle) => (tangentVector u).ofLp i

Each coordinate of the frame tangent is continuous in the angle.

theorem MovingSofa.norm_tangentVector (t : Real.Angle) :

‖tangentVector t‖ = 1

The frame tangent is a unit vector.

theorem MovingSofa.norm_tangentVector_coordinate_le_one (t : Real.Angle) (i : Fin 2) :

‖(tangentVector t).ofLp i‖ ≤ 1

Each coordinate of the frame tangent is bounded by one.

Geometry / Normal Lines #

theorem MovingSofa.eq_of_inner_sub_normalVector_eq_zero_of_ne {a b : Point} {s t : ℝ} (hs : s ∈ Set.Ioo 0 Real.pi) (ht : t ∈ Set.Ioo 0 Real.pi) (hab : a ≠ b) (horths : inner ℝ (b - a) (normalVector ↑s) = 0) (hortht : inner ℝ (b - a) (normalVector ↑t) = 0) :

s = t

A nontrivial segment has at most one normal direction strictly between zero and pi.

theorem MovingSofa.normalLine_eq_iff_of_mem_Ioo {s t c d : ℝ} (hs : s ∈ Set.Ioo 0 Real.pi) (ht : t ∈ Set.Ioo 0 Real.pi) :

normalLine (↑s) c = normalLine (↑t) d ↔ s = t ∧ c = d

Normal lines with angles strictly between zero and pi agree exactly when their data agree.

theorem MovingSofa.normalLine_eq_of_cut {a b c : ℝ} (hab : ↑b = ↑(a + Real.pi)) :

normalLine (↑b) c = normalLine (↑a) (-c)

Opposite normal angles describe the same line with the opposite offset.

Geometry / Quadrant Bounds #

theorem MovingSofa.isBounded_setOf_le_snd_and_inner_lt (a b c t : ℝ) (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) :

Bornology.IsBounded {p : Point | a ≤ p.ofLp 1 ∧ inner ℝ p (normalVector ↑t) < b ∧ inner ℝ p (normalVector ↑(t + Real.pi / 2)) < c}

A horizontal lower bound cuts a first-quadrant pair of upper projection bounds to a bounded set.

The planar region under the graph of a function #

For a b : ℝ and f : ℝ → ℝ this file describes the three planar regions between the horizontal axis and the graph of f over [a, b]: closedSubgraph, which contains both the base segment and the graph, strictSubgraph, which contains the base but not the graph, and openSubgraph, which contains neither.

For a function continuous on [a, b], vanishing at a and b and positive in between, the closed region is the closure of either smaller region (closure_openSubgraph, closure_strictSubgraph) and the open region is its interior (interior_closedSubgraph).

theorem MovingSofa.Point.eq_vecNotation (z : Point) :

z = !₂[z.ofLp 0, z.ofLp 1]

A planar point is recovered from its two coordinates.

def MovingSofa.closedSubgraph (a b : ℝ) (f : ℝ → ℝ) :

The closed region between the base and the graph of f over [a, b].

Equations

MovingSofa.closedSubgraph a b f = {q : MovingSofa.Point | a ≤ q.ofLp 0 ∧ q.ofLp 0 ≤ b ∧ 0 ≤ q.ofLp 1 ∧ q.ofLp 1 ≤ f (q.ofLp 0)}

Instances For

def MovingSofa.strictSubgraph (a b : ℝ) (f : ℝ → ℝ) :

The region under the graph of f over [a, b], including the base but not the graph.

Equations

MovingSofa.strictSubgraph a b f = {q : MovingSofa.Point | a ≤ q.ofLp 0 ∧ q.ofLp 0 ≤ b ∧ 0 ≤ q.ofLp 1 ∧ q.ofLp 1 < f (q.ofLp 0)}

Instances For

def MovingSofa.openSubgraph (a b : ℝ) (f : ℝ → ℝ) :

The open region strictly between the base and the graph of f over (a, b).

Equations

MovingSofa.openSubgraph a b f = {q : MovingSofa.Point | a < q.ofLp 0 ∧ q.ofLp 0 < b ∧ 0 < q.ofLp 1 ∧ q.ofLp 1 < f (q.ofLp 0)}

Instances For

theorem MovingSofa.openSubgraph_subset_strictSubgraph {a b : ℝ} {f : ℝ → ℝ} :

openSubgraph a b f ⊆ strictSubgraph a b f

The open subgraph omits the base, which the strict subgraph contains.

theorem MovingSofa.strictSubgraph_subset_closedSubgraph {a b : ℝ} {f : ℝ → ℝ} :

strictSubgraph a b f ⊆ closedSubgraph a b f

The strict subgraph omits the graph, which the closed subgraph contains.

theorem MovingSofa.openSubgraph_subset_closedSubgraph {a b : ℝ} {f : ℝ → ℝ} :

openSubgraph a b f ⊆ closedSubgraph a b f

The open subgraph is contained in the closed one.

theorem MovingSofa.isClosed_closedSubgraph {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) :

IsClosed (closedSubgraph a b f)

The closed subgraph of a function continuous on the base interval is closed.

theorem MovingSofa.isOpen_openSubgraph {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) :

IsOpen (openSubgraph a b f)

The open subgraph of a function continuous on the base interval is open.

theorem MovingSofa.closure_openSubgraph {a b : ℝ} {f : ℝ → ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (ha : f a = 0) (hb : f b = 0) (hpos : ∀ x ∈ Set.Ioo a b, 0 < f x) :

closure (openSubgraph a b f) = closedSubgraph a b f

The closed subgraph is the closure of the open one: interior graph points are limits from below, base points at interior horizontal coordinates are limits from above, and the two corners are limits of half-height points over the open base interval.

theorem MovingSofa.interior_closedSubgraph {a b : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) (ha : f a = 0) (hb : f b = 0) :

interior (closedSubgraph a b f) = openSubgraph a b f

The open subgraph is the interior of the closed one.

theorem MovingSofa.closure_strictSubgraph {a b : ℝ} {f : ℝ → ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (ha : f a = 0) (hb : f b = 0) (hpos : ∀ x ∈ Set.Ioo a b, 0 < f x) :

closure (strictSubgraph a b f) = closedSubgraph a b f

The closed subgraph is also the closure of the strict subgraph.

Geometry / Support #

theorem MovingSofa.exists_mem_inner_eq_supportValue (K : ConvexBody Point) (t : Real.Angle) :

∃ p ∈ ↑K, inner ℝ p (normalVector t) = supportValue (↑K) t

A compact convex body attains its support value in every normal direction.

theorem MovingSofa.supportValue_image_add_of_isCompact {s : Set Point} (hs : IsCompact s) (hne : s.Nonempty) (v : Point) (t : Real.Angle) :

supportValue ((fun (p : Point) => p + v) '' s) t = supportValue s t + inner ℝ v (normalVector t)

Translating a nonempty compact set adds the normal component to its support value.

theorem MovingSofa.supportValue_image_add (K : ConvexBody Point) (v : Point) (t : Real.Angle) :

supportValue ((fun (p : Point) => p + v) '' ↑K) t = supportValue (↑K) t + inner ℝ v (normalVector t)

Translating a compact convex body adds the normal component of the translation to support.

theorem MovingSofa.inner_le_supportValue_of_isCompact {s : Set Point} (hs : IsCompact s) {p : Point} (hp : p ∈ s) (a : Real.Angle) :

inner ℝ p (normalVector a) ≤ supportValue s a

Every point of a compact set lies below its support value.

theorem MovingSofa.inner_le_supportValue (K : ConvexBody Point) {p : Point} (hp : p ∈ K) (t : Real.Angle) :

inner ℝ p (normalVector t) ≤ supportValue (↑K) t

A point of a convex body lies below each supporting line.

theorem MovingSofa.supportValue_le_of_subset_normalHalfPlane (K : ConvexBody Point) (t : Real.Angle) (c : ℝ) (hK : ↑K ⊆ normalHalfPlane t c false false) :

supportValue (↑K) t ≤ c

Containment in a closed normal half-plane bounds the support value.

theorem MovingSofa.supportValue_eq_of_subset_of_inner_le {s u : Set Point} (hs : s.Nonempty) (hsu : s ⊆ u) (a : Real.Angle) (hu : ∀ p ∈ u, inner ℝ p (normalVector a) ≤ supportValue s a) :

supportValue u a = supportValue s a

Enlarging a nonempty set without increasing its directional upper bound preserves support.

theorem MovingSofa.exists_mem_inner_eq_of_convex {s : Set Point} (hconv : Convex ℝ s) {A C : Point} (hA : A ∈ s) (hC : C ∈ s) {u : Point} {c : ℝ} (hCle : inner ℝ C u ≤ c) (hAge : c ≤ inner ℝ A u) :

∃ q ∈ s, inner ℝ q u = c

A convex set meets every intermediate level of a linear functional.

theorem MovingSofa.supportValue_le_of_cut {s : Set Point} (hne : s.Nonempty) {a b c : ℝ} (hab : ↑b = ↑(a + Real.pi)) (hs : ∀ p ∈ s, c ≤ inner ℝ p (normalVector ↑a)) :

supportValue s ↑b ≤ -c

Support bound in the direction opposite to a cut line lying below the set.

theorem MovingSofa.le_supportValue_of_cut {s : Set Point} (hcomp : IsCompact s) {a b c : ℝ} {p : Point} (hab : ↑b = ↑(a + Real.pi)) (hp : p ∈ s) (hpc : inner ℝ p (normalVector ↑a) = c) :

-c ≤ supportValue s ↑b

A contact point on a cut line attains the opposite support value.

Geometry / Contacts #

def MovingSofa.exposedEdge (K : ConvexBody Point) (t : Real.Angle) :

The exposed edge at a normal direction, including singleton edges.

Equations

MovingSofa.exposedEdge K t = ↑K ∩ (MovingSofa.supportingLineHalfPlane (↑K) t).1

Instances For

noncomputable def MovingSofa.edgeVertices (K : ConvexBody Point) (t : Real.Angle) :

Point × Point

The positive and negative tangent endpoints of an exposed edge.

Equations

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

Instances For

noncomputable def MovingSofa.supportingIntersection (K : ConvexBody Point) (a b : Real.Angle) :

Point

The intersection point of two supporting lines at nonparallel normal directions.

Equations

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

Instances For

theorem MovingSofa.exposedEdge_nonempty (K : ConvexBody Point) (t : Real.Angle) :

(exposedEdge K t).Nonempty

theorem MovingSofa.convex_exposedEdge (K : ConvexBody Point) (t : Real.Angle) :

Convex ℝ (exposedEdge K t)

theorem MovingSofa.isConnected_exposedEdge (K : ConvexBody Point) (t : Real.Angle) :

IsConnected (exposedEdge K t)

theorem MovingSofa.supportingIntersection_inner_left (K : ConvexBody Point) (s t : ℝ) :

inner ℝ (supportingIntersection K ↑s ↑t) (normalVector ↑s) = supportValue ↑K ↑s

theorem MovingSofa.supportingIntersection_inner_right (K : ConvexBody Point) (s t : ℝ) (h : Real.sin (t - s) ≠ 0) :

inner ℝ (supportingIntersection K ↑s ↑t) (normalVector ↑t) = supportValue ↑K ↑t

theorem MovingSofa.supportingIntersection_comm (K : ConvexBody Point) (s t : ℝ) (h : Real.sin (t - s) ≠ 0) :

supportingIntersection K ↑s ↑t = supportingIntersection K ↑t ↑s

theorem MovingSofa.isCompact_exposedEdge (K : ConvexBody Point) (t : Real.Angle) :

IsCompact (exposedEdge K t)

Every exposed edge of a compact convex body is compact.

theorem MovingSofa.edgeVertices_fst_mem (K : ConvexBody Point) (t : Real.Angle) :

(edgeVertices K t).1 ∈ exposedEdge K t

The positive tangent endpoint belongs to its exposed edge.

theorem MovingSofa.edgeVertices_snd_mem (K : ConvexBody Point) (t : Real.Angle) :

(edgeVertices K t).2 ∈ exposedEdge K t

The negative tangent endpoint belongs to its exposed edge.

theorem MovingSofa.edgeVertices_eq_of_exposedEdge_singleton {K : ConvexBody Point} {t : Real.Angle} {p : Point} (h : exposedEdge K t = {p}) :

edgeVertices K t = (p, p)

A singleton exposed face is both of its tangent endpoints.

theorem MovingSofa.inner_edgeVertices_fst_tangent (K : ConvexBody Point) (t : Real.Angle) :

inner ℝ (edgeVertices K t).1 (tangentVector t) = sSup ((fun (p : Point) => inner ℝ p (tangentVector t)) '' exposedEdge K t)

The positive face vertex attains the largest tangent coordinate.

theorem MovingSofa.inner_edgeVertices_snd_tangent (K : ConvexBody Point) (t : Real.Angle) :

inner ℝ (edgeVertices K t).2 (tangentVector t) = sInf ((fun (p : Point) => inner ℝ p (tangentVector t)) '' exposedEdge K t)

The negative face vertex attains the smallest tangent coordinate.

theorem MovingSofa.exposedEdge_eq_segment_edgeVertices (K : ConvexBody Point) (t : Real.Angle) :

exposedEdge K t = segment ℝ (edgeVertices K t).2 (edgeVertices K t).1

An exposed face is the segment joining its two tangent-extreme vertices.

theorem MovingSofa.edgeVertices_eq_of_exposedEdge_eq (K L : ConvexBody Point) (u : Real.Angle) (h : exposedEdge K u = exposedEdge L u) :

edgeVertices K u = edgeVertices L u

An exposed face determines the support value and both of its endpoint vertices.

theorem MovingSofa.supportingIntersection_eq_edgeVertices_snd_of_mem (K : ConvexBody Point) {a b : ℝ} (hab : 0 < b - a) (hpi : b - a < Real.pi) (hp : supportingIntersection K ↑a ↑b ∈ K) :

supportingIntersection K ↑a ↑b = (edgeVertices K ↑b).2

A support-line intersection in the body is the negative endpoint at the later normal.

theorem MovingSofa.supportingIntersection_eq_edgeVertices_fst_of_mem (K : ConvexBody Point) {a b : ℝ} (hab : 0 < b - a) (hpi : b - a < Real.pi) (hp : supportingIntersection K ↑a ↑b ∈ K) :

supportingIntersection K ↑a ↑b = (edgeVertices K ↑a).1

A support-line intersection in the body is the positive endpoint at the earlier normal.

theorem MovingSofa.supportingIntersection_eq_fst_add_pos_tangent (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hba : b < a + Real.pi) (hne : (edgeVertices K ↑a).1 ≠ (edgeVertices K ↑b).2) :

∃ (d : ℝ), 0 < d ∧ supportingIntersection K ↑a ↑b = (edgeVertices K ↑a).1 + d • tangentVector ↑a

The first endpoint reaches the adjacent supporting-line intersection along a positive tangent ray.

theorem MovingSofa.supportingIntersection_eq_snd_sub_pos_tangent (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hba : b < a + Real.pi) (hne : (edgeVertices K ↑a).1 ≠ (edgeVertices K ↑b).2) :

∃ (d : ℝ), 0 < d ∧ supportingIntersection K ↑a ↑b = (edgeVertices K ↑b).2 - d • tangentVector ↑b

The second endpoint reaches the adjacent supporting-line intersection against a positive tangent ray.

Faces at a reversed normal direction #

theorem MovingSofa.supportValue_add_pi_eq_neg_of_forall_le {L : ConvexBody Point} {c t : ℝ} {p : Point} (hle : ∀ q ∈ ↑L, c ≤ inner ℝ q (normalVector ↑t)) (hp : p ∈ ↑L) (hpc : inner ℝ p (normalVector ↑t) = c) :

supportValue ↑L ↑(t + Real.pi) = -c

A body bounded below in a normal direction, with the bound attained, has the opposite support value in the reversed direction.

theorem MovingSofa.exposedEdge_add_pi_eq_of_forall_le {L : ConvexBody Point} {c t : ℝ} {p : Point} (hle : ∀ q ∈ ↑L, c ≤ inner ℝ q (normalVector ↑t)) (hp : p ∈ ↑L) (hpc : inner ℝ p (normalVector ↑t) = c) :

exposedEdge L ↑(t + Real.pi) = {q : Point | q ∈ ↑L ∧ inner ℝ q (normalVector ↑t) = c}

The face at a reversed normal direction consists of the points attaining the attained lower bound.

Faces between two supporting normals with a common contact point #

theorem MovingSofa.eq_supportingIntersection_of_mem_exposedEdge {L : ConvexBody Point} {a b : ℝ} {p : Point} (hsin : Real.sin (a - b) ≠ 0) (hpa : p ∈ exposedEdge L ↑a) (hpb : p ∈ exposedEdge L ↑b) :

p = supportingIntersection L ↑a ↑b

A point on two transverse supporting lines is their intersection.

theorem MovingSofa.exposedEdge_eq_singleton_of_mem_exposedEdge_of_mem_Ioo {L : ConvexBody Point} {a b s : ℝ} {p : Point} (hba : b < a + Real.pi) (hs : s ∈ Set.Ioo a b) (hpa : p ∈ exposedEdge L ↑a) (hpb : p ∈ exposedEdge L ↑b) :

exposedEdge L ↑s = {p}

Between two supporting normals less than a straight angle apart with a common contact point, every intervening face is that point.

Geometry / Frame Calculus #

theorem MovingSofa.hasDerivAt_normalVector (t : ℝ) :

HasDerivAt (fun (s : ℝ) => normalVector ↑s) (tangentVector ↑t) t

theorem MovingSofa.hasDerivAt_tangentVector (t : ℝ) :

HasDerivAt (fun (s : ℝ) => tangentVector ↑s) (-normalVector ↑t) t

theorem MovingSofa.lipschitzWith_normalVector_real :

LipschitzWith 1 fun (t : ℝ) => normalVector ↑t

The angular unit-normal parametrization is one-Lipschitz.

theorem MovingSofa.lipschitzWith_tangentVector_real :

LipschitzWith 1 fun (t : ℝ) => tangentVector ↑t

The angular unit-tangent parametrization is one-Lipschitz.

theorem MovingSofa.lipschitzOnWith_frameCombination {f g : ℝ → ℝ} {C M : ℝ} {D : NNReal} {s : Set ℝ} (hD : 2 * (C + M) ≤ ↑D) (hM : 0 ≤ M) (hf : ∀ (x y : ℝ), |f x - f y| ≤ C * |x - y|) (hg : ∀ (x y : ℝ), |g x - g y| ≤ C * |x - y|) (hfM : ∀ x ∈ s, |f x| ≤ M) (hgM : ∀ x ∈ s, |g x| ≤ M) :

LipschitzOnWith D (fun (x : ℝ) => f x • normalVector ↑x + g x • tangentVector ↑x) s

A combination of the rotating frame whose coefficients are globally Lipschitz and bounded on a set is Lipschitz on that set.

theorem MovingSofa.hasDerivAt_inner_normalVector (A : Point) (t : ℝ) :

HasDerivAt (fun (u : ℝ) => inner ℝ A (normalVector ↑u)) (inner ℝ A (tangentVector ↑t)) t

The angular derivative of a fixed normal projection is its tangent projection.

theorem MovingSofa.exists_contact_of_hasDerivAt {s : Set Point} (hcomp : IsCompact s) (hne : s.Nonempty) {t d : ℝ} (hd : HasDerivAt (fun (u : ℝ) => supportValue s ↑u) d t) :

∃ A ∈ s, inner ℝ A (normalVector ↑t) = supportValue s ↑t ∧ inner ℝ A (tangentVector ↑t) = d

A contact point in a normal direction has the support derivative as tangent coordinate.

Cap.Basic.
Cap.AngleDomain.
Cap.Area.

Cap / Basic #

def MovingSofa.capUpperAngles (ω : ℝ) :

Set ℝ

The two real intervals of upper cap normals.

Equations

MovingSofa.capUpperAngles ω = Set.Icc 0 ω ∪ Set.Icc (Real.pi / 2) (ω + Real.pi / 2)

Instances For

def MovingSofa.capLowerNormals (ω : ℝ) :

Set Real.Angle

The normal directions of the two lower strip boundaries.

Equations

MovingSofa.capLowerNormals ω = {↑(ω + Real.pi), ↑(3 * Real.pi / 2)}

Instances For

def MovingSofa.HasHalfPlaneRepresentation (s : Set Point) (normals : Set Real.Angle) :

A set represented by closed lower half-planes with allowed normal directions.

Equations

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

Instances For

def MovingSofa.IsCap (ω : ℝ) (K : ConvexBody Point) :

The normalized cap conditions, including its nonzero rotation-angle domain.

Equations

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

Instances For

def MovingSofa.CapSpace (ω : ℝ) :

The space of caps at a fixed rotation angle.

Equations

MovingSofa.CapSpace ω = { K : ConvexBody MovingSofa.Point // MovingSofa.IsCap ω K }

Instances For

structure MovingSofa.AngleSet :

A nonempty finite set of angles strictly between zero and its rotation angle.

angle : ℝ
The terminal rotation angle of the polygonal approximation.
angle_pos : 0 < self.angle
angle_le : self.angle ≤ Real.pi / 2
directions : Finset ℝ
The finite nonempty set of interior wall directions.
nonempty : self.directions.Nonempty
interior (t : ℝ) : t ∈ self.directions → t ∈ Set.Ioo 0 self.angle

Instances For

def MovingSofa.angleDomain (Θ : AngleSet) :

Set ℝ

The finite upper-normal domain associated with an angle set.

Equations

MovingSofa.angleDomain Θ = ↑Θ.directions ∪ (fun (t : ℝ) => t + Real.pi / 2) '' ↑Θ.directions ∪ {Θ.angle, Real.pi / 2}

Instances For

def MovingSofa.PolygonCapSpace (Θ : AngleSet) :

Polygon caps whose upper normals belong to the specified angle domain.

Equations

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

Instances For

def MovingSofa.capFan (ω : ℝ) :

The fan above both lower strip boundaries.

Equations

MovingSofa.capFan ω = MovingSofa.normalHalfPlane (↑ω) 0 true false ∩ MovingSofa.normalHalfPlane (↑(Real.pi / 2)) 0 true false

Instances For

theorem MovingSofa.convex_capFan (ω : ℝ) :

Convex ℝ (capFan ω)

The fan of a rotation angle is convex.

def MovingSofa.innerQuadrant (s : Set Point) (t : ℝ) :

The open inward quadrant of the supporting hallway, in support coordinates.

Equations

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

Instances For

theorem MovingSofa.convex_innerQuadrant (s : Set Point) (t : ℝ) :

Convex ℝ (innerQuadrant s t)

The open inward quadrant of a supporting hallway is convex.

def MovingSofa.capNiche {ω : ℝ} (K : CapSpace ω) :

The niche is the union of inward quadrants clipped by the fan.

Equations

MovingSofa.capNiche K = MovingSofa.capFan ω ∩ ⋃ t ∈ Set.Ioo 0 ω, MovingSofa.innerQuadrant (↑↑K) t

Instances For

def MovingSofa.polygonNiche (Θ : AngleSet) (K : CapSpace Θ.angle) :

The finite-angle niche uses the same fan clipping as the continuous niche.

Equations

MovingSofa.polygonNiche Θ K = MovingSofa.capFan Θ.angle ∩ ⋃ t ∈ Θ.directions, MovingSofa.innerQuadrant (↑↑K) t

Instances For

theorem MovingSofa.notMem_innerQuadrant_iff (S : Set Point) (u : ℝ) (p : Point) :

p ∉ innerQuadrant S u ↔ p ∈ normalHalfPlane (↑u) (supportValue S ↑u - 1) true false ∨ p ∈ normalHalfPlane (↑(u + Real.pi / 2)) (supportValue S ↑(u + Real.pi / 2) - 1) true false

Avoiding an inward quadrant means lying above one of its two inner walls.

Cap / Angle Domain #

theorem MovingSofa.angleDomain_subset_Ioo (Θ : AngleSet) :

angleDomain Θ ⊆ Set.Ioo 0 Real.pi

Every upper normal of an angle set has strictly positive sine.

Cap / Area #

noncomputable def MovingSofa.capAreaFunctional {ω : ℝ} (K : CapSpace ω) :

Cap area minus niche area, with real Lebesgue area as in the classical interface.

Equations

MovingSofa.capAreaFunctional K = MovingSofa.ClassicalResults.area ↑↑K - MovingSofa.ClassicalResults.area (MovingSofa.capNiche K)

Instances For

@[reducible, inline]

abbrev MovingSofa.RightAngleCapSpace :

The cap space at a right angle.

Equations

MovingSofa.RightAngleCapSpace = MovingSofa.CapSpace (Real.pi / 2)

Instances For

noncomputable def MovingSofa.rightAngleAreaFunctional (K : RightAngleCapSpace) :

The sofa area functional on the right-angle cap space.

Equations

MovingSofa.rightAngleAreaFunctional K = MovingSofa.capAreaFunctional K

Instances For

Polygon.AngleSet.
Polygon.BooleanFunctions.
Polygon.Height.Space.
Polygon.Height.Bounds.
Polygon.Height.RaisedSupport.
Polygon.Nef.Basic.
Polygon.Nef.CapConstruction.
Polygon.Nef.Cells.
Polygon.Nef.Height.
Polygon.PerturbationBounds.
Polygon.Polyline.Basic.
Polygon.Polyline.Displacement.
Polygon.Polyline.Graph.
Polygon.Polyline.Measure.
Polygon.Polyline.Projection.

Polygon / Angle Set #

noncomputable def MovingSofa.uniformAngleSet (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (n : ℕ) (hn : 2 ≤ n) :

AngleSet

The interior points of the uniform angular grid.

Equations

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

Instances For

theorem MovingSofa.uniformAngleSet_directions_mono_of_dvd (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) {m n : ℕ} (hm : 2 ≤ m) (hn : 2 ≤ n) (hmn : m ∣ n) :

(uniformAngleSet ω hω hω' m hm).directions ⊆ (uniformAngleSet ω hω hω' n hn).directions

A divisible grid refines the original grid.

theorem MovingSofa.uniformAngleSet_directions_mono_of_dyadic (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (n : ℕ → ℕ) (hn : ∀ (i : ℕ), 2 ≤ n i) (hmono : Monotone n) (hdyadic : ∀ (i : ℕ), ∃ (k : ℕ), n i = 2 ^ k) {i j : ℕ} (hij : i ≤ j) :

(uniformAngleSet ω hω hω' (n i) ⋯).directions ⊆ (uniformAngleSet ω hω hω' (n j) ⋯).directions

Monotone dyadic grids have nested directions.

theorem MovingSofa.exists_uniformAngleSet_mem_Ioo (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (n : ℕ) (hn : 2 ≤ n) {a b : ℝ} (ha : 0 ≤ a) (hb : b ≤ ω) (hmesh : ω / ↑n < b - a) :

∃ t ∈ (uniformAngleSet ω hω hω' n hn).directions, t ∈ Set.Ioo a b

An interval longer than the mesh contains a grid direction.

theorem MovingSofa.eventually_exists_uniformAngleSet_mem_Ioo (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (n : ℕ → ℕ) (hn : ∀ (i : ℕ), 2 ≤ n i) (hmono : StrictMono n) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b ≤ ω) :

∀ᶠ (i : ℕ) in Filter.atTop , ∃ t ∈ (uniformAngleSet ω hω hω' (n i) ⋯).directions, t ∈ Set.Ioo a b

An increasing sequence of grids eventually meets each interior open interval.

Polygon / Boolean Functions #

@[reducible, inline]

abbrev MovingSofa.BooleanFunction (n : ℕ) :

Boolean functions of finitely many Boolean variables.

Equations

MovingSofa.BooleanFunction n = ((Fin n → Bool) → Bool)

Instances For

def MovingSofa.IsMonotoneBooleanFunction {n : ℕ} (E : BooleanFunction n) :

Changing inputs from false to true cannot change a true output to false.

Equations

MovingSofa.IsMonotoneBooleanFunction E = ∀ (P Q : Fin n → Bool), (∀ (i : Fin n), P i = true → Q i = true) → E P = true → E Q = true

Instances For

inductive MovingSofa.PositiveBooleanFormula (n : ℕ) :

Formulas built from variables using only conjunction and disjunction.

variable {n : ℕ} (i : Fin n) : PositiveBooleanFormula n
conjunction {n : ℕ} (left right : PositiveBooleanFormula n) : PositiveBooleanFormula n
disjunction {n : ℕ} (left right : PositiveBooleanFormula n) : PositiveBooleanFormula n

Instances For

def MovingSofa.PositiveBooleanFormula.eval {n : ℕ} :

PositiveBooleanFormula n → BooleanFunction n

Evaluate a positive formula under a Boolean assignment.

Equations

(MovingSofa.PositiveBooleanFormula.variable i).eval = fun (P : Fin n → Bool) => P i
(left.conjunction right).eval = fun (P : Fin n → Bool) => left.eval P && right.eval P
(left.disjunction right).eval = fun (P : Fin n → Bool) => left.eval P || right.eval P

Instances For

IsMonotoneBooleanFunction E.eval

theorem MovingSofa.positiveBooleanFormula_monotone {n : ℕ} (E : PositiveBooleanFormula n) :

Polygon / Height / Space #

def MovingSofa.PolygonCapTranslateSpace (Θ : AngleSet) :

Point sets obtained by translating a polygonal cap with the fixed angle data.

Equations

MovingSofa.PolygonCapTranslateSpace Θ = { S : Set MovingSofa.Point // ∃ (K : MovingSofa.PolygonCapSpace Θ) (q : MovingSofa.Point), S = (fun (p : MovingSofa.Point) => p + q) '' ↑↑↑K }

Instances For

def MovingSofa.PolygonHeightSpace (Θ : AngleSet) :

Real wall heights indexed by the finite angle domain.

Equations

MovingSofa.PolygonHeightSpace Θ = (↑(MovingSofa.angleDomain Θ) → ℝ)

Instances For

noncomputable def MovingSofa.polygonHeightValue {Θ : AngleSet} (h : PolygonHeightSpace Θ) (t : ℝ) :

Extend a wall-height function by zero outside its angle domain.

Equations

MovingSofa.polygonHeightValue h t = if ht : t ∈ MovingSofa.angleDomain Θ then h ⟨t, ht⟩ else 0

Instances For

def MovingSofa.polygonHeightParallelogram {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Intersect the two endpoint strips of unit width determined by the height data.

Equations

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

Instances For

def MovingSofa.polygonHeightCap {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Cut the endpoint parallelogram by all upper wall half-planes.

Equations

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

Instances For

def MovingSofa.polygonHeightFan {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Intersect the lower half-planes at the two endpoint directions.

Equations

MovingSofa.polygonHeightFan h = ⋂ t ∈ {Θ.angle, Real.pi / 2}, MovingSofa.normalHalfPlane (↑t) (MovingSofa.polygonHeightValue h t - 1) true false

Instances For

def MovingSofa.polygonHeightNiche {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Intersect the endpoint fan with the union of forbidden inner corners.

Equations

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

Instances For

noncomputable def MovingSofa.polygonHeightArea {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

The real area of the cap minus the real area of its niche.

Equations

MovingSofa.polygonHeightArea h = MovingSofa.ClassicalResults.area (MovingSofa.polygonHeightCap h) - MovingSofa.ClassicalResults.area (MovingSofa.polygonHeightNiche h)

Instances For

noncomputable def MovingSofa.polygonHeightExtensions {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Set Point × Set Point × Set Point × Set Point × ℝ

Bundle the parallelogram, cap, fan, niche and area constructed from wall heights.

Equations

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

Instances For

noncomputable def MovingSofa.polygonTranslateHeight {Θ : AngleSet} (K : PolygonCapTranslateSpace Θ) :

PolygonHeightSpace Θ

Take support values of a translated cap in the prescribed directions.

Equations

MovingSofa.polygonTranslateHeight K t = MovingSofa.supportValue ↑K ↑↑t

Instances For

noncomputable def MovingSofa.polygonTranslateExtensions {Θ : AngleSet} (K : PolygonCapTranslateSpace Θ) :

Set Point × ℝ

The niche and area functional associated with a translated cap.

Equations

MovingSofa.polygonTranslateExtensions K = (MovingSofa.polygonHeightNiche (MovingSofa.polygonTranslateHeight K), MovingSofa.polygonHeightArea (MovingSofa.polygonTranslateHeight K))

Instances For

Polygon / Height / Bounds #

theorem MovingSofa.polygonHeightCap_subset_normalHalfPlane {Θ : AngleSet} (h : PolygonHeightSpace Θ) {t : ℝ} (ht : t ∈ angleDomain Θ) :

polygonHeightCap h ⊆ normalHalfPlane (↑t) (polygonHeightValue h t) false false

A height cap satisfies each selected upper half-plane constraint.

theorem MovingSofa.supportValue_le_polygonHeightValue {Θ : AngleSet} (h : PolygonHeightSpace Θ) (K : ConvexBody Point) (hK : polygonHeightCap h = ↑K) {t : ℝ} (ht : t ∈ angleDomain Θ) :

supportValue ↑K ↑t ≤ polygonHeightValue h t

The support of a reconstructed height cap is bounded by each defining height.

theorem MovingSofa.supportValue_eq_polygonHeightValue_of_width_one {Θ : AngleSet} (h : PolygonHeightSpace Θ) (K : ConvexBody Point) (hK : polygonHeightCap h = ↑K) {t : ℝ} (ht : t ∈ {Θ.angle, Real.pi / 2}) (hw : supportValue ↑K ↑t + supportValue ↑K ↑(t + Real.pi) = 1) :

supportValue ↑K ↑t = polygonHeightValue h t

Unit width forces equality with the height of a distinguished strip.

theorem MovingSofa.polygonHeightNiche_mono_of_eq_endpoints {Θ : AngleSet} {h g : PolygonHeightSpace Θ} (hle : ∀ (t : ↑(angleDomain Θ)), h t ≤ g t) (heq : ∀ t ∈ {Θ.angle, Real.pi / 2}, polygonHeightValue h t = polygonHeightValue g t) :

polygonHeightNiche h ⊆ polygonHeightNiche g

Niches grow with their heights when the fan remains fixed.

theorem MovingSofa.isBounded_polygonHeightNiche {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Bornology.IsBounded (polygonHeightNiche h)

Every polygon height niche is bounded.

Polygon / Height / Raised Support #

noncomputable def MovingSofa.raisedPolygonSupport {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ε : ℝ) :

PolygonHeightSpace Θ

Increase one selected support height by the prescribed amount.

Equations

MovingSofa.raisedPolygonSupport K t ε s = MovingSofa.supportValue ↑↑↑K ↑↑s + if s = t then ε else 0

Instances For

Polygon / Nef / Basic #

structure MovingSofa.PlanarHalfPlaneData :

Normal direction, height and boundary conventions specifying a planar half-plane.

angle : Real.Angle
The angle of the half-plane’s normal vector.
height : ℝ
The scalar-product threshold defining the boundary line.
upper : Bool
Select the side above the threshold when true, or below it when false.
strict : Bool
Exclude the boundary line when true.

Instances For

def MovingSofa.PlanarHalfPlaneData.carrier (H : PlanarHalfPlaneData) :

The half-plane defined by the recorded normal, threshold and conventions.

Equations

H.carrier = MovingSofa.normalHalfPlane H.angle H.height H.upper H.strict

Instances For

def MovingSofa.PlanarHalfPlaneData.boundaryLine (H : PlanarHalfPlaneData) :

The line where the normal scalar product equals the recorded height.

Equations

H.boundaryLine = MovingSofa.normalLine H.angle H.height

Instances For

def MovingSofa.booleanSet {n : ℕ} (E : BooleanFunction n) (H : Fin n → Set Point) :

Evaluate a Boolean function on the point’s memberships in a finite family of sets.

Equations

MovingSofa.booleanSet E H = {p : MovingSofa.Point | (E fun (i : Fin n) => decide (p ∈ H i)) = true }

Instances For

def MovingSofa.IsNefPolygon (X : Set Point) :

The set is a finite Boolean combination of planar half-planes.

Equations

MovingSofa.IsNefPolygon X = ∃ (n : ℕ) (E : MovingSofa.BooleanFunction n) (H : Fin n → MovingSofa.PlanarHalfPlaneData), X = MovingSofa.booleanSet E fun (i : Fin n) => (H i).carrier

Instances For

def MovingSofa.IsSimpleNefPolygonWith {n : ℕ} (X : Set Point) (H : Fin n → PlanarHalfPlaneData) :

A monotone Boolean representation uses the supplied walls with distinct boundary lines.

Equations

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

Instances For

Polygon / Nef / Cap Construction #

def MovingSofa.polygonCapWalls {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Set PlanarHalfPlaneData

The upper walls and two lower endpoint walls defining the polygonal cap.

Equations

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

Instances For

def MovingSofa.polygonNicheWalls {Θ : AngleSet} (h : PolygonHeightSpace Θ) :

Set PlanarHalfPlaneData

The strict inner walls and two lower endpoint walls defining the polygonal niche.

Equations

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

Instances For

theorem MovingSofa.polygonCap_niche_simpleNef (Θ : AngleSet) (h : PolygonHeightSpace Θ) :

(∃ (n : ℕ) (H : Fin n → PlanarHalfPlaneData), Set.range H = polygonCapWalls h ∧ IsSimpleNefPolygonWith (polygonHeightCap h) H) ∧ ∃ (n : ℕ) (H : Fin n → PlanarHalfPlaneData), Set.range H = polygonNicheWalls h ∧ IsSimpleNefPolygonWith (polygonHeightNiche h) H

Polygon / Nef / Cells #

theorem MovingSofa.Nef.monotoneBoolean_update_false {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (P : Fin n → Bool) (i : Fin n) :

E (Function.update P i false) = true → E P = true

theorem MovingSofa.Nef.monotoneBoolean_update_true {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (P : Fin n → Bool) (i : Fin n) :

E P = true → E (Function.update P i true) = true

theorem MovingSofa.Nef.monotoneBoolean_eval_iff {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (P : Fin n → Bool) (i : Fin n) :

E P = true ↔ E (Function.update P i false) = true ∨ P i = true ∧ E (Function.update P i true) = true

theorem MovingSofa.Nef.booleanSet_update_eq {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → Set Point) (i : Fin n) (S : Set Point) :

booleanSet E (Function.update H i S) = booleanSet E (Function.update H i ∅) ∪ S ∩ booleanSet E (Function.update H i Set.univ)

theorem MovingSofa.Nef.booleanSet_update_sdiff {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → Set Point) (i : Fin n) (S T : Set Point) :

booleanSet E (Function.update H i S) \ booleanSet E (Function.update H i T) = S \ T ∩ (booleanSet E (Function.update H i Set.univ) \ booleanSet E (Function.update H i ∅))

theorem MovingSofa.Nef.booleanSet_mono {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) {H G : Fin n → Set Point} (hHG : ∀ (i : Fin n), H i ⊆ G i) :

booleanSet E H ⊆ booleanSet E G

def MovingSofa.Nef.booleanCell {n : ℕ} (H : Fin n → Set Point) (P : Fin n → Bool) :

The points realizing exactly the specified Boolean membership pattern.

Equations

MovingSofa.Nef.booleanCell H P = ⋂ (j : Fin n), if P j = true then H j else (H j)ᶜ

Instances For

noncomputable def MovingSofa.Nef.setMembershipPattern {n : ℕ} (H : Fin n → Set Point) (p : Point) :

Fin n → Bool

The vector of membership decisions for a point in a finite set family.

Equations

MovingSofa.Nef.setMembershipPattern H p j = decide (p ∈ H j)

Instances For

theorem MovingSofa.Nef.mem_booleanCell_iff {n : ℕ} (H : Fin n → Set Point) (P : Fin n → Bool) (p : Point) :

p ∈ booleanCell H P ↔ setMembershipPattern H p = P

theorem MovingSofa.Nef.booleanSet_eq_iUnion_booleanCell {n : ℕ} (E : BooleanFunction n) (H : Fin n → Set Point) :

booleanSet E H = ⋃ (P : Fin n → Bool), if E P = true then booleanCell H P else ∅

def MovingSofa.Nef.closedBooleanCell {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) :

Intersect the closed sides of each wall selected by the Boolean pattern.

Equations

MovingSofa.Nef.closedBooleanCell H P = ⋂ (j : Fin n), MovingSofa.normalHalfPlane (H j).angle (H j).height (if P j = true then (H j).upper else !(H j).upper) false

Instances For

theorem MovingSofa.Nef.mem_booleanCell_iff_mem_closedBooleanCell_of_ne {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (p : Point) (hp : ∀ (j : Fin n), inner ℝ p (normalVector (H j).angle) ≠ (H j).height) :

p ∈ booleanCell (fun (j : Fin n) => (H j).carrier) P ↔ p ∈ closedBooleanCell H P

def MovingSofa.Nef.IsActiveBooleanPattern {n : ℕ} (E : BooleanFunction n) (i : Fin n) (P : Fin n → Bool) :

Switching the selected input from false to true switches the output to true.

Equations

MovingSofa.Nef.IsActiveBooleanPattern E i P = (E (Function.update P i false) = false ∧ E (Function.update P i true) = true)

Instances For

noncomputable def MovingSofa.Nef.activeBooleanPatterns {n : ℕ} (E : BooleanFunction n) (i : Fin n) :

Finset (Fin n → Bool)

All input patterns for which the selected Boolean variable is active.

Equations

MovingSofa.Nef.activeBooleanPatterns E i = Finset.filter (MovingSofa.Nef.IsActiveBooleanPattern E i) Finset.univ

Instances For

def MovingSofa.Nef.activeBooleanRegion {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) :

The set gained by making the selected wall universally true rather than false.

Equations

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

Instances For

theorem MovingSofa.Nef.mem_activeBooleanRegion_iff {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (p : Point) :

p ∈ activeBooleanRegion E H i ↔ IsActiveBooleanPattern E i (setMembershipPattern (fun (j : Fin n) => (H j).carrier) p)

theorem MovingSofa.Nef.measurableSet_planarHalfPlane_carrier (H : PlanarHalfPlaneData) :

MeasurableSet H.carrier

theorem MovingSofa.Nef.eventually_mem_carrier_iff_of_not_mem_boundaryLine (H : PlanarHalfPlaneData) (p : Point) (hp : p ∉ H.boundaryLine) :

∀ᶠ (q : Point) in nhds p, q ∈ H.carrier ↔ p ∈ H.carrier

theorem MovingSofa.Nef.eventually_setMembershipPattern_eq_of_ne {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (p : Point) (hp : ∀ (j : Fin n), j ≠ i → p ∉ (H j).boundaryLine) :

∀ᶠ (q : Point) in nhds p, ∀ (j : Fin n), j ≠ i → setMembershipPattern (fun (k : Fin n) => (H k).carrier) q j = setMembershipPattern (fun (k : Fin n) => (H k).carrier) p j

theorem MovingSofa.Nef.measurableSet_booleanCell {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) :

MeasurableSet (booleanCell (fun (j : Fin n) => (H j).carrier) P)

theorem MovingSofa.Nef.measurableSet_booleanSet {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) :

MeasurableSet (booleanSet E fun (j : Fin n) => (H j).carrier)

theorem MovingSofa.Nef.monotoneBoolean_update_false_true {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (i : Fin n) (P : Fin n → Bool) :

E (Function.update P i false) = true → E (Function.update P i true) = true

theorem MovingSofa.Nef.not_isActiveBooleanPattern_iff {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (i : Fin n) (P : Fin n → Bool) :

¬IsActiveBooleanPattern E i P ↔ E (Function.update P i false) = E (Function.update P i true)

Polygon / Nef / Height #

def MovingSofa.perturbNefHeight {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (δ : ℝ) :

Change one wall’s height by δ in a Boolean half-plane representation.

Equations

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

Instances For

theorem MovingSofa.Nef.perturbNefHeight_eq_update {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (δ : ℝ) :

perturbNefHeight E H i δ = booleanSet E (Function.update (fun (j : Fin n) => (H j).carrier) i (have __src := H i; { angle := __src.angle, height := (H i).height + δ, upper := __src.upper, strict := __src.strict }).carrier)

theorem MovingSofa.Nef.perturbNefHeight_sdiff {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (δ ε : ℝ) :

perturbNefHeight E H i δ \ perturbNefHeight E H i ε = (have __src := H i; { angle := __src.angle, height := (H i).height + δ, upper := __src.upper, strict := __src.strict }).carrier \ (have __src := H i; { angle := __src.angle, height := (H i).height + ε, upper := __src.upper, strict := __src.strict }).carrier ∩ (booleanSet E (Function.update (fun (j : Fin n) => (H j).carrier) i Set.univ) \ booleanSet E (Function.update (fun (j : Fin n) => (H j).carrier) i ∅))

def MovingSofa.Nef.heightInterval (strict : Bool) (h δ ε : ℝ) :

Set ℝ

The half-open strip-height interval matching the wall’s strictness convention.

Equations

MovingSofa.Nef.heightInterval strict h δ ε = if strict = true then Set.Ico (h + ε) (h + δ) else Set.Ioc (h + ε) (h + δ)

Instances For

theorem MovingSofa.Nef.measurableSet_heightInterval (strict : Bool) (h δ ε : ℝ) :

MeasurableSet (heightInterval strict h δ ε)

theorem MovingSofa.Nef.integral_heightInterval_eq_intervalIntegral (strict : Bool) (h δ ε : ℝ) (f : ℝ → ℝ) (hεδ : ε ≤ δ) :

∫ (x : ℝ) in heightInterval strict h δ ε, f x = ∫ (x : ℝ) in h + ε..h + δ, f x

theorem MovingSofa.Nef.mem_heightInterval_bounds {strict : Bool} {h δ ε x : ℝ} (hx : x ∈ heightInterval strict h δ ε) :

h + ε ≤ x ∧ x ≤ h + δ

theorem MovingSofa.Nef.carrier_sdiff_carrier_eq_heightInterval (H : PlanarHalfPlaneData) (hSide : H.upper = false) (δ ε : ℝ) :

{ angle := H.angle, height := H.height + δ, upper := H.upper, strict := H.strict }.carrier \ { angle := H.angle, height := H.height + ε, upper := H.upper, strict := H.strict }.carrier = {p : Point | inner ℝ p (normalVector H.angle) ∈ heightInterval H.strict H.height δ ε}

theorem MovingSofa.Nef.perturbNefHeight_sdiff_eq_heightInterval {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (δ ε : ℝ) :

perturbNefHeight E H i δ \ perturbNefHeight E H i ε = {p : Point | inner ℝ p (normalVector (H i).angle) ∈ heightInterval (H i).strict (H i).height δ ε} ∩ (booleanSet E (Function.update (fun (j : Fin n) => (H j).carrier) i Set.univ) \ booleanSet E (Function.update (fun (j : Fin n) => (H j).carrier) i ∅))

theorem MovingSofa.Nef.perturbNefHeight_mono {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) :

Monotone (perturbNefHeight E H i)

theorem MovingSofa.Nef.measurableSet_perturbNefHeight {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (δ : ℝ) :

MeasurableSet (perturbNefHeight E H i δ)

theorem MovingSofa.Nef.area_perturb_sub_eq_volume_sdiff {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (R ε₀ δ ε : ℝ) (hεδ : ε ≤ δ) (hδ : |δ| ≤ ε₀) (hε : |ε| ≤ ε₀) (hBound : ∀ (z : ℝ), |z| ≤ ε₀ → perturbNefHeight E H i z ⊆ Metric.closedBall 0 R) :

ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i ε) = (MeasureTheory.volume (perturbNefHeight E H i δ \ perturbNefHeight E H i ε)).toReal

theorem MovingSofa.Nef.perturbNefHeight_zero {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) :

perturbNefHeight E H i 0 = booleanSet E fun (j : Fin n) => (H j).carrier

Polygon / Perturbation Bounds #

def MovingSofa.independentWallCap {Θ : AngleSet} (upper lower : PolygonHeightSpace Θ) :

The polygonal cap with independently specified upper and lower wall heights.

Equations

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

Instances For

def MovingSofa.independentWallNiche {Θ : AngleSet} (lower : PolygonHeightSpace Θ) :

The polygonal niche determined by independently specified lower wall heights.

Equations

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

Instances For

theorem MovingSofa.polygonPerturbation_uniform_bounds (Θ : AngleSet) (h : PolygonHeightSpace Θ) :

∃ (R : ℝ) (ε₀ : ℝ), 0 < R ∧ 0 < ε₀ ∧ ∀ (upper lower : PolygonHeightSpace Θ), (∀ (t : ↑(angleDomain Θ)), |upper t - h t| ≤ ε₀) → (∀ (t : ↑(angleDomain Θ)), |lower t - (h t - 1)| ≤ ε₀) → independentWallCap upper lower ⊆ Metric.closedBall 0 R ∧ independentWallNiche lower ⊆ Metric.closedBall 0 R

Polygon / Polyline / Basic #

structure MovingSofa.XMonotonePolylineData :