Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-23 11:21 5b2c9521

View on Github →

feat(analysis/convex.cone): prove M. Riesz extension theorem, Hahn-Banach theorem (#2120)

  • feat(analysis/convex.cone): prove M. Riesz extension theorem WIP
  • Complete the proof TODO: move many facts to linear_algebra/basic, fix possible build failures in other files
  • Fix compile of analysis/convex/cone
  • Cleanup, rewrite using linear_pmaps
  • Deduce Hahn-Banach theorem from M. Riesz extension theorem
  • Fix lint
  • Apply suggestions from code review [skip_ci] Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Expand comments, prove properties of convex.to_cone.
  • Docstrings
  • Apply suggestions from code review Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Update src/analysis/convex/cone.lean
  • Update src/linear_algebra/basic.lean

Estimated changes

added theorem smul_eq_zero
added theorem submodule.coe_mk
modified theorem submodule.coe_sub
added theorem convex_iff_forall_pos
added theorem convex.mem_to_cone'
added theorem convex.mem_to_cone
added theorem convex.subset_to_cone
added def convex.to_cone
added theorem convex.to_cone_eq_Inf
added theorem convex_cone.add_mem
added theorem convex_cone.coe_inf
added theorem convex_cone.comap_id
added theorem convex_cone.convex
added theorem convex_cone.ext'
added theorem convex_cone.ext
added def convex_cone.map
added theorem convex_cone.map_id
added theorem convex_cone.map_map
added theorem convex_cone.mem_Inf
added theorem convex_cone.mem_bot
added theorem convex_cone.mem_coe
added theorem convex_cone.mem_comap
added theorem convex_cone.mem_inf
added theorem convex_cone.mem_mk
added theorem convex_cone.mem_top
added theorem convex_cone.smul_mem
added structure convex_cone
added theorem riesz_extension.step
added theorem riesz_extension
added theorem set.bex_image_iff
added theorem set_coe.exists'
added theorem linear_equiv.prod_symm
added theorem submodule.coe_of_le
modified theorem submodule.of_le_apply
added def linear_pmap.comp
added theorem linear_pmap.domain_sup
added theorem linear_pmap.fst_apply
added theorem linear_pmap.map_add
added theorem linear_pmap.map_neg
added theorem linear_pmap.map_smul
added theorem linear_pmap.map_sub
added theorem linear_pmap.map_zero
added theorem linear_pmap.mk_apply
added theorem linear_pmap.neg_apply
added theorem linear_pmap.snd_apply
added theorem linear_pmap.sup_apply
added structure linear_pmap
added theorem subtype.coe_prop
added theorem directed.mono
deleted theorem directed_mono
added theorem directed_on.mono
added theorem directed_on_image