LeanPool.Monsky.TriangleCorollary

Imported Lean Pool material for LeanPool.Monsky.TriangleCorollary.

noncomputable def LeanPool.Monsky.idMapEquiv : EuclideanSpace ℝ (Fin 2) ≃ᵐ ℝ × ℝ

The measurable equivalence ℝ² ≃ᵐ ℝ × ℝ unfolding a Euclidean plane vector to a pair.

Equations

• LeanPool.Monsky.idMapEquiv = (MeasurableEquiv.toLp 2 (Fin 2 → ℝ)).symm.trans MeasurableEquiv.finTwoArrow

noncomputable def LeanPool.Monsky.idMap : EuclideanSpace ℝ (Fin 2) → ℝ × ℝ

The underlying function of idMapEquiv.

Equations

• LeanPool.Monsky.idMap = ⇑LeanPool.Monsky.idMapEquiv

theorem LeanPool.Monsky.measure_image_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α ≃ᵐ β} (hf : MeasureTheory.MeasurePreserving (⇑f) μa μb) (s : Set α) : μa s = μb (⇑f '' s)

theorem LeanPool.Monsky.map_pres (X : Set (EuclideanSpace ℝ (Fin 2))) : MeasureTheory.volume X = MeasureTheory.volume (idMap '' X)

@[simp]

theorem LeanPool.Monsky.idMap_apply (x : EuclideanSpace ℝ (Fin 2)) : idMap x = (x.ofLp 0, x.ofLp 1)

idMap sends a Euclidean plane vector to the pair of its coordinates.

def LeanPool.Monsky.unitTriangle : Fin 3 → EuclideanSpace ℝ (Fin 2)

The unit triangle with vertices (0,0), (1,0) and (0,1).

Equations

• LeanPool.Monsky.unitTriangle 0 = LeanPool.Monsky.v 0 0
• LeanPool.Monsky.unitTriangle 1 = LeanPool.Monsky.v 1 0
• LeanPool.Monsky.unitTriangle 2 = LeanPool.Monsky.v 0 1

theorem LeanPool.Monsky.unitTriangle_def : unitTriangle = fun (x : Fin 3) => match x with | 0 => v 0 0 | 1 => v 1 0 | 2 => v 0 1

def LeanPool.Monsky.lower : ℝ → ℝ

The lower boundary function (constantly zero) of the unit triangle region.

Equations

• LeanPool.Monsky.lower = 0

def LeanPool.Monsky.upper : ℝ → ℝ

The upper boundary function x ↦ 1 - x of the unit triangle region.

Equations

• LeanPool.Monsky.upper x = 1 - x

theorem LeanPool.Monsky.unit_is_unit_in_prod : idMap '' openHull unitTriangle = regionBetween lower upper (Set.Ioc 0 1)

theorem LeanPool.Monsky.unit_in_prod_is_unit : idMap ⁻¹' regionBetween lower upper (Set.Ioc 0 1) = openHull unitTriangle

theorem LeanPool.Monsky.volume_open_unitTriangle : MeasureTheory.volume (openHull unitTriangle) = 1 / 2

theorem LeanPool.Monsky.volume_open_unitTriangle1 : (MeasureTheory.volume (openHull unitTriangle)).toReal = 1 / 2

theorem LeanPool.Monsky.measurable_unitTriangle : MeasurableSet (openHull unitTriangle)

theorem LeanPool.Monsky.area_lin_map (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) (A : Set (EuclideanSpace ℝ (Fin 2))) : MeasureTheory.volume (⇑L '' A) = ENNReal.ofReal |LinearMap.det L| * MeasureTheory.volume A

def LeanPool.Monsky.translation (a : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)

Translation of the plane by a fixed vector a.

Equations

• LeanPool.Monsky.translation a x = x + a

theorem LeanPool.Monsky.area_translation (a : EuclideanSpace ℝ (Fin 2)) (A : Set (EuclideanSpace ℝ (Fin 2))) : MeasureTheory.volume (translation a '' A) = MeasureTheory.volume A

theorem LeanPool.Monsky.lincom_commutes (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) {n : ℕ} (a : Fin n → ℝ) (f : Fin n → EuclideanSpace ℝ (Fin 2)) : ∑ i : Fin n, a i • L (f i) = L (∑ i : Fin n, a i • f i)

theorem LeanPool.Monsky.openHull_lin_trans (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) {n : ℕ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) : openHull (⇑L ∘ f) = ⇑L '' openHull f

theorem LeanPool.Monsky.closedHull_lin_trans (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) {n : ℕ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) : closedHull (⇑L ∘ f) = ⇑L '' closedHull f

theorem LeanPool.Monsky.aux_for_translation {n : ℕ} {f : Fin n → EuclideanSpace ℝ (Fin 2)} {a : Fin n → ℝ} {b : EuclideanSpace ℝ (Fin 2)} (h1 : a ∈ openSimplex n) : ∑ i : Fin n, a i • (f i + b) = ∑ i : Fin n, a i • f i + b

theorem LeanPool.Monsky.translation_commutes {n : ℕ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) (b : EuclideanSpace ℝ (Fin 2)) : openHull (translation b ∘ f) = translation b '' openHull f

theorem LeanPool.Monsky.aux_for_translation_closed {n : ℕ} {f : Fin n → EuclideanSpace ℝ (Fin 2)} {a : Fin n → ℝ} {b : EuclideanSpace ℝ (Fin 2)} (h1 : a ∈ closedSimplex n) : ∑ i : Fin n, a i • (f i + b) = ∑ i : Fin n, a i • f i + b

theorem LeanPool.Monsky.translation_commutes_closed {n : ℕ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) (b : EuclideanSpace ℝ (Fin 2)) : closedHull (translation b ∘ f) = translation b '' closedHull f

noncomputable def LeanPool.Monsky.ourBasis : Module.Basis (Fin 2) ℝ (EuclideanSpace ℝ (Fin 2))

The standard basis of the Euclidean plane used throughout.

Equations

• LeanPool.Monsky.ourBasis = PiLp.basisFun 2 ℝ (Fin 2)

noncomputable def LeanPool.Monsky.ourBasisOrtho : OrthonormalBasis (Fin 2) ℝ (EuclideanSpace ℝ (Fin 2))

The standard orthonormal basis of the Euclidean plane.

Equations

• LeanPool.Monsky.ourBasisOrtho = EuclideanSpace.basisFun (Fin 2) ℝ

theorem LeanPool.Monsky.ourBasisOrtho_zero : ourBasisOrtho 0 = !₂[1, 0]

The first standard orthonormal basis vector of the plane is (1, 0).

theorem LeanPool.Monsky.ourBasisOrtho_one : ourBasisOrtho 1 = !₂[0, 1]

The second standard orthonormal basis vector of the plane is (0, 1).

noncomputable def LeanPool.Monsky.basisTransform (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Fin 2 → EuclideanSpace ℝ (Fin 2)

The pair of edge vectors of a triangle from its first vertex.

Equations

• LeanPool.Monsky.basisTransform T 0 = T 1 - T 0
• LeanPool.Monsky.basisTransform T 1 = T 2 - T 0

noncomputable def LeanPool.Monsky.linearTransform (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)

The linear map sending the standard basis to a triangle's edge vectors.

Equations

• LeanPool.Monsky.linearTransform T = (LeanPool.Monsky.ourBasis.constr ℝ) (LeanPool.Monsky.basisTransform T)

def LeanPool.Monsky.triangleTranslation (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)

Translation by the first vertex of a triangle.

Equations

• LeanPool.Monsky.triangleTranslation T = LeanPool.Monsky.translation (T 0)

theorem LeanPool.Monsky.ourBasis_def : ourBasis = PiLp.basisFun 2 ℝ (Fin 2)

theorem LeanPool.Monsky.basisTransform_def (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : basisTransform T = fun (x : Fin 2) => match x with | 0 => T 1 - T 0 | 1 => T 2 - T 0

theorem LeanPool.Monsky.linearTransform_def (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : linearTransform T = (ourBasis.constr ℝ) (basisTransform T)

theorem LeanPool.Monsky.triangleTranslation_def (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : triangleTranslation T = translation (T 0)

theorem LeanPool.Monsky.unitTriangle_to_triangle (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : triangleTranslation T '' ⇑(linearTransform T) '' openHull unitTriangle = openHull T

theorem LeanPool.Monsky.half_is_half : 2⁻¹ = ENNReal.ofReal 2⁻¹

theorem LeanPool.Monsky.volume_open_triangle' (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : MeasureTheory.volume (openHull T) = ENNReal.ofReal (|det T| / 2)

theorem LeanPool.Monsky.volume_open_triangle (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : (MeasureTheory.volume (openHull T)).toReal = |det T| / 2

noncomputable def LeanPool.Monsky.unitSegment : Fin 2 → EuclideanSpace ℝ (Fin 2)

The unit segment from (0,0) to (0,1).

Equations

• LeanPool.Monsky.unitSegment 0 = LeanPool.Monsky.v 0 0
• LeanPool.Monsky.unitSegment 1 = LeanPool.Monsky.v 1 0

noncomputable def LeanPool.Monsky.yAxis : Submodule ℝ (EuclideanSpace ℝ (Fin 2))

The y-axis as a submodule of the plane.

Equations

• LeanPool.Monsky.yAxis = Submodule.span ℝ (Set.range LeanPool.Monsky.unitSegment)

theorem LeanPool.Monsky.unitSegment_def : unitSegment = fun (x : Fin 2) => match x with | 0 => v 0 0 | 1 => v 1 0

theorem LeanPool.Monsky.yAxis_def : yAxis = Submodule.span ℝ (Set.range unitSegment)

theorem LeanPool.Monsky.closed_unitSegment_subset : closedHull unitSegment ⊆ ↑yAxis

theorem LeanPool.Monsky.volume_closed_unitSegment : MeasureTheory.volume (closedHull unitSegment) = 0

noncomputable def LeanPool.Monsky.basisTransformSegment (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : Fin 2 → EuclideanSpace ℝ (Fin 2)

The edge vector of a segment together with the zero vector.

Equations

• LeanPool.Monsky.basisTransformSegment L 0 = L 1 - L 0
• LeanPool.Monsky.basisTransformSegment L 1 = 0

noncomputable def LeanPool.Monsky.linearTransformSegment (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)

The linear map sending the standard basis to a segment's edge vector.

Equations

• LeanPool.Monsky.linearTransformSegment L = (LeanPool.Monsky.ourBasis.constr ℝ) (LeanPool.Monsky.basisTransformSegment L)

def LeanPool.Monsky.segmentTranslation (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)

Translation by the first endpoint of a segment.

Equations

• LeanPool.Monsky.segmentTranslation L = LeanPool.Monsky.translation (L 0)

theorem LeanPool.Monsky.basisTransformSegment_def (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : basisTransformSegment L = fun (x : Fin 2) => match x with | 0 => L 1 - L 0 | 1 => 0

theorem LeanPool.Monsky.linearTransformSegment_def (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : linearTransformSegment L = (ourBasis.constr ℝ) (basisTransformSegment L)

theorem LeanPool.Monsky.segmentTranslation_def (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : segmentTranslation L = translation (L 0)

theorem LeanPool.Monsky.unitSegment_toSegment (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : segmentTranslation L '' ⇑(linearTransformSegment L) '' closedHull unitSegment = closedHull L

theorem LeanPool.Monsky.volume_closed_segment (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : MeasureTheory.volume (closedHull L) = 0

theorem LeanPool.Monsky.box_equal_to_pare : parallelepiped ⇑ourBasisOrtho = closedHull unitSquare

theorem LeanPool.Monsky.volume_box : (MeasureTheory.volume (closedHull unitSquare)).toReal = 1

theorem LeanPool.Monsky.det_of_triangle_transform (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : LinearMap.det (linearTransform T) = det T

theorem LeanPool.Monsky.nondegen_triangle_lin_inv (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : LinearMap.det (linearTransform T) ≠ 0

noncomputable def LeanPool.Monsky.bijLinearTransform (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : EuclideanSpace ℝ (Fin 2) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin 2)

The linear equivalence given by a nondegenerate triangle's linear transform.

Equations

• LeanPool.Monsky.bijLinearTransform T h = (LeanPool.Monsky.linearTransform T).equivOfDetNeZero ⋯

theorem LeanPool.Monsky.linearTransform_bij (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : Function.Bijective ⇑(linearTransform T)

theorem LeanPool.Monsky.linearTransform_bij_left_inf (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : Function.LeftInverse ⇑(linearTransform T) ⇑(bijLinearTransform T h).symm

def LeanPool.Monsky.invTriangleTranslation (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)

The inverse of triangleTranslation, translating by the negated first vertex.

Equations

• LeanPool.Monsky.invTriangleTranslation T = LeanPool.Monsky.translation (-T 0)

theorem LeanPool.Monsky.translation_bijective (a : EuclideanSpace ℝ (Fin 2)) : Function.Bijective (translation a)

theorem LeanPool.Monsky.triangleTranslation_bijective (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Function.Bijective (triangleTranslation T)

theorem LeanPool.Monsky.inv_translation_left (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Function.LeftInverse (triangleTranslation T) (invTriangleTranslation T)

theorem LeanPool.Monsky.pre_unitTriangle_to_triangle (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : ⇑(linearTransform T) ⁻¹' triangleTranslation T ⁻¹' openHull T = openHull unitTriangle

theorem LeanPool.Monsky.pre_triangle_to_unitTriangle (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : invTriangleTranslation T ⁻¹' ⇑(bijLinearTransform T h).symm ⁻¹' openHull unitTriangle = openHull T

theorem LeanPool.Monsky.meas_lin_map (L : EuclideanSpace ℝ (Fin 2) →ₗ[ℝ] EuclideanSpace ℝ (Fin 2)) : Measurable ⇑L

theorem LeanPool.Monsky.meas_translation (a : EuclideanSpace ℝ (Fin 2)) : Measurable (translation a)

theorem LeanPool.Monsky.meas_invTriangleTranslation (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Measurable (invTriangleTranslation T)

theorem LeanPool.Monsky.nondegen_triangle_meas (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) (h : det T ≠ 0) : MeasurableSet (openHull T)

theorem LeanPool.Monsky.null_meas_triangle (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : MeasureTheory.NullMeasurableSet (openHull T) MeasureTheory.volume

def LeanPool.Monsky.allEdgesTriangleHull (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Set (EuclideanSpace ℝ (Fin 2))

The union of the closed hulls of a triangle's three sides.

Equations

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

theorem LeanPool.Monsky.closed_triangle_is_union (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : closedHull T = openHull T ∪ allEdgesTriangleHull T

theorem LeanPool.Monsky.volume_zero (A B : Set (EuclideanSpace ℝ (Fin 2))) (h : MeasureTheory.volume B = 0) : MeasureTheory.volume (A ∪ B) = MeasureTheory.volume A

theorem LeanPool.Monsky.allEdgesTriangleHull_area (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : MeasureTheory.volume (allEdgesTriangleHull T) = 0

theorem LeanPool.Monsky.union_of_edges_zero_vol (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) : MeasureTheory.volume (⋃ T ∈ S, allEdgesTriangleHull T) = 0

theorem LeanPool.Monsky.area_equal_sum_cover (X : Set (EuclideanSpace ℝ (Fin 2))) (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hcover : isDisjointCover X ↑S) : MeasureTheory.volume X = ∑ T ∈ S, MeasureTheory.volume (openHull T)

theorem LeanPool.Monsky.triangle_det_sum_one (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hcover : isDisjointCover (closedHull unitSquare) ↑S) : ∑ T ∈ S, |det T| / 2 = 1

theorem LeanPool.Monsky.equal_area_cover_implies_triangleArea_n (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hcover : isEqualAreaCover (closedHull unitSquare) ↑S) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : T ∈ S → triangleArea T = 1 / ↑S.card