TwoProfileGeometry.lean

1import BFPP.TwoProfiles2import BFPP.ProfileGeometry3import Mathlib.Analysis.Normed.Module.Convex45/-! # The coefficient domain as a closed bounded convex subset of a Banach space -/67namespace BFPP89set_option autoImplicit false1011open Set1213universe u v14variable {ι : Type u} {κ : Type v}15  [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ]1617def twoProfileSet (ι : Type u) (κ : Type v)18    [LinearOrder ι] [OrderBot ι] [LinearOrder κ] [OrderBot κ] :19    Set (BoundedFamily ι × BoundedFamily κ) :=20  {z | z.1 ∈ profileSet ι ∧ z.2 ∈ profileSet κ ∧21    2 ≤ BoundedFamily.supremum z.1 + BoundedFamily.supremum z.2}2223theorem twoProfileSet_isClosed : IsClosed (twoProfileSet ι κ) := by24  have h₁ : IsClosed {z : BoundedFamily ι × BoundedFamily κ | z.1 ∈ profileSet ι} :=25    (profileSet_isClosed (ι := ι)).preimage continuous_fst26  have h₂ : IsClosed {z : BoundedFamily ι × BoundedFamily κ | z.2 ∈ profileSet κ} :=27    (profileSet_isClosed (ι := κ)).preimage continuous_snd28  have h₃ : IsClosed {z : BoundedFamily ι × BoundedFamily κ |29      2 ≤ BoundedFamily.supremum z.1 + BoundedFamily.supremum z.2} :=30    isClosed_le continuous_const31      ((BoundedFamily.supremum_nonexpansive.continuous.comp continuous_fst).add32        (BoundedFamily.supremum_nonexpansive.continuous.comp continuous_snd))33  exact h₁.inter (h₂.inter h₃)3435theorem twoProfileSet_convex : Convex ℝ (twoProfileSet ι κ) := by36  intro x hx y hy r s hr hs hrs37  refine ⟨profileSet_convex hx.1 hy.1 hr hs hrs,38    profileSet_convex hx.2.1 hy.2.1 hr hs hrs, ?_⟩39  let a : Profile ι := ⟨x.1, hx.1⟩40  let a' : Profile ι := ⟨y.1, hy.1⟩41  let b : Profile κ := ⟨x.2, hx.2.1⟩42  let b' : Profile κ := ⟨y.2, hy.2.1⟩43  change 2 ≤ (a.mix a' r s hr hs hrs).tail + (b.mix b' r s hr hs hrs).tail44  rw [Profile.tail_mix, Profile.tail_mix]45  have hx' : 2 ≤ a.tail + b.tail := hx.2.246  have hy' : 2 ≤ a'.tail + b'.tail := hy.2.247  have h₁ := mul_le_mul_of_nonneg_left hx' hr48  have h₂ := mul_le_mul_of_nonneg_left hy' hs49  nlinarith5051theorem twoProfileSet_norm_le (z : BoundedFamily ι × BoundedFamily κ)52    (hz : z ∈ twoProfileSet ι κ) : ‖z‖ ≤ 2 := by53  change max ‖z.1‖ ‖z.2‖ ≤ 254  exact max_le (Profile.norm_le_two ⟨z.1, hz.1⟩)55    (Profile.norm_le_two ⟨z.2, hz.2.1⟩)5657theorem twoProfileSet_isBounded : Bornology.IsBounded (twoProfileSet ι κ) := by58  apply (Metric.isBounded_closedBall (x := (0 : BoundedFamily ι × BoundedFamily κ)) (r := 2)).subset59  intro z hz60  simpa only [Metric.mem_closedBall, dist_zero_right] using twoProfileSet_norm_le z hz6162noncomputable def TwoProfile.witness [NoMaxOrder ι] [NoMaxOrder κ] : TwoProfile ι κ :=63  ⟨(Profile.stepOne, Profile.stepOne), by simp only [Profile.tail_stepOne]; norm_num⟩6465theorem twoProfileSet_nonempty [NoMaxOrder ι] [NoMaxOrder κ] :66    (twoProfileSet ι κ).Nonempty := by67  let z : TwoProfile ι κ := TwoProfile.witness68  exact ⟨(z.val.1.val, z.val.2.val), z.val.1.property, z.val.2.property, z.property⟩6970/-- The two presentations of the domain have exactly the same metric. -/71def TwoProfile.ambientEquiv : TwoProfile ι κ ≃ {z // z ∈ twoProfileSet ι κ} where72  toFun z := ⟨(z.val.1.val, z.val.2.val), z.val.1.property, z.val.2.property, z.property⟩73  invFun z := ⟨(⟨z.val.1, z.property.1⟩, ⟨z.val.2, z.property.2.1⟩), z.property.2.2⟩74  left_inv _ := rfl75  right_inv _ := rfl7677theorem TwoProfile.ambientEquiv_isometry :78    Isometry (TwoProfile.ambientEquiv : TwoProfile ι κ → {z // z ∈ twoProfileSet ι κ}) :=79  fun _ _ => rfl8081end BFPP

SHA-256