TwoProfileStructure.lean

1import BFPP.TwoProfileGeometry23/-! # Completeness and convex combinations of the two-profile domain -/45namespace BFPP.TwoProfile67set_option autoImplicit false89universe u v10variable {ι : Type u} {κ : Type v}11  [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]1213instance : CompleteSpace (TwoProfile ι κ) := by14  letI : CompleteSpace {z // z ∈ twoProfileSet ι κ} := twoProfileSet_isClosed.completeSpace_coe15  let e : TwoProfile ι κ ≃ᵢ {z // z ∈ twoProfileSet ι κ} :=16    ⟨ambientEquiv, ambientEquiv_isometry⟩17  exact e.completeSpace_iff.mpr inferInstance1819noncomputable def mix (z w : TwoProfile ι κ) (r s : ℝ)20    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) : TwoProfile ι κ := by21  refine ⟨(z.val.1.mix w.val.1 r s hr hs hrs, z.val.2.mix w.val.2 r s hr hs hrs), ?_⟩22  rw [Profile.tail_mix, Profile.tail_mix]23  have h₁ := mul_le_mul_of_nonneg_left z.property hr24  have h₂ := mul_le_mul_of_nonneg_left w.property hs25  nlinarith2627@[simp] theorem mix_first (z w : TwoProfile ι κ) (r s : ℝ)28    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) :29    (z.mix w r s hr hs hrs).val.1 = z.val.1.mix w.val.1 r s hr hs hrs := rfl3031@[simp] theorem mix_second (z w : TwoProfile ι κ) (r s : ℝ)32    (hr : 0 ≤ r) (hs : 0 ≤ s) (hrs : r + s = 1) :33    (z.mix w r s hr hs hrs).val.2 = z.val.2.mix w.val.2 r s hr hs hrs := rfl3435end BFPP.TwoProfile

SHA-256