Existance proof of a sequence inductively (Banach Dieudonné)

Stream: mathlib4

[Christopher Hoskin]

I'm attempting to prove the Banach Dieudonné theorem using Mathlib4. The proof of this requires the following lemma:

universe u

/- More generally could consider a locally convex metrizable space -/
variable {𝕜₁ : Type u} [RCLike 𝕜₁]
variable {E₁ : Type u} [NormedAddCommGroup E₁] [NormedSpace 𝕜₁ E₁]

/- The closed set, not containing the origin -/
variable (C : Set (WeakDual 𝕜₁ E₁))

/-- More generally could consider a decreasing sequence of fundamental neighbourhoods of 0 -/
def U : ℕ → Set E
  | 0 => univ
  | n => ball 0 n⁻¹

theorem exists_seq_finite_subsets (hC₁ : IsClosed C) (hC₂ : 0 ∉ C): ∃ F : ℕ → Set E₁, ∀ n : ℕ,
    (F n).Finite ∧ F n ⊆ (U n) ∧ polar 𝕜₁ (⋃₀ {F k | k ≤ n }) ∩ polar 𝕜₁ (U (n + 1)) ∩ C = ∅ :=
  sorry

That is to say, show the existence of a (non-unique) sequence of sets F n in a Banach space E with the following properties:

F n ⊆ U n

polar 𝕜 (⋃₀ {F k | k ≤ n }) ∩ polar 𝕜 (U (n + 1)) ∩ C = ∅

where C is a weak*-closed subset of the dual of E not containing the origin and U n is the sequence of open balls of radius n at the origin.

After a lot of thrashing around, I think I have formalized the proof of the inductive step :

variable (n : ℕ)

/- Placeholder for union Fⱼ 0 ≤ j ≤ m-/
variable (s : Set E₁)

lemma existance [ProperSpace 𝕜₁] (hC₁ : IsClosed C)
    (h : polar 𝕜₁ s ∩ C ∩ polar 𝕜₁ (U (n+1)) = ∅) :
    ∃ F, F.Finite ∧ F ⊆ (U (E := E₁) (n + 1)) ∧
      polar 𝕜₁ (s ∪ F) ∩ C ∩ polar 𝕜₁ (U (n+2)) = ∅ := sorry

See https://github.com/leanprover-community/mathlib4/pull/16316 for the details (currently the proof is a right mess - I had a lot of difficult applying results like Set.inter_iInter to the output of isCompact_iff_finite_subfamily_closed).

However, I'm not sure how to feed this existance lemma into the proof of exists_seq_finite_subsets to complete the proof of the lemma.

Please could someone give me a few pointers as to how to advance this?

Thanks,

Christopher

[Edward van de Meent]

i think the easiest way to do this would be to use a mutual section where you define such a sequence using Exists.Choose, and immediately prove that this sequence has the properties you seek.

[Edward van de Meent]

alternatively, you could define a partial ordering on sequences with l ≤ r := for all N, if up to N, l has the relevant property, then l and r agree up to N (and as a result r has the relevant property up to at least N). Then, use zorns lemma to prove that there is a maximal sequence, which must have the relevant property for all n by an inductive argument

[Edward van de Meent]

more concretely:

zorns lemma approach

import Mathlib.Order.Zorn

universe u v

variable {α : Type u} [Preorder α] {β :α → Type v} (P : ((a:α) → β a) → α → Prop)

def rel : ((a:α) → β a) → ((a:α) → β a) → Prop := fun l r =>
  ∀ N, (∀ n ≤ N, P l n) → ((∀ n ≤ N, l n = r n) ∧ (∀ n ≤ N, P r n))

instance : IsRefl ((a:α) → β a) (rel P) where
  refl := by
    intro a
    dsimp [rel]
    intro _ h
    constructor
    · exact fun _ _ => rfl
    · exact h

instance : IsTrans ((a:α) → β a) (rel P) where
  trans := by
    intro a b c
    dsimp [rel]
    intro hab hbc N f
    specialize hab N f
    specialize hbc N hab.right
    constructor
    · intro n hn
      exact (hab.left n hn).trans (hbc.left n hn)
    · exact hbc.right


open Classical in
noncomputable def choose_ub [∀ a, Nonempty (β a)] (c : Set ((a:α) → β a)) :
    ((a:α) → β a) :=
  fun N =>
    if h: ∃ x ∈ c, ∀ n ≤ N, P x n then
      h.choose N
    else
      Classical.choice (‹∀ a, Nonempty (β a)› N)

lemma exists_ub [∀ a, Nonempty (β a)]
    (hP : ∀ (l r : ((a:α) → β a)), ∀ (N:α),
      (∀ n ≤ N, P l n) → (∀ n ≤ N, l n = r n) → ∀ n ≤ N, P r n):
    ∀ (c : Set ((a:α) → β a)), IsChain (rel P) c →
      ∃ (ub : ((a:α) → β a)), ∀ a ∈ c, (rel P) a ub := by
  intro c hc
  use choose_ub P c
  intro x hx
  dsimp [rel,choose_ub]
  intro N hx_prop
  constructor
  · intro n hn
    have : ∃ x' ∈ c, ∀ n_1 ≤ n, P x' n_1 := by
      use x, hx
      intro n_1 hn_1
      exact hx_prop n_1 (hn_1.trans hn)
    rw [dif_pos this]
    obtain hy := this.choose_spec
    revert hy
    generalize this.choose = y
    intro hy
    obtain (l|r) := hc.total hx hy.left
    · specialize l N hx_prop
      exact l.left n hn
    · specialize r n hy.right
      exact (r.left n (le_refl n)).symm
  · intro n hn
    apply hP x (choose_ub P c) N hx_prop _ n hn
    dsimp [choose_ub]
    intro n hn
    have : ∃ x' ∈ c, ∀ n_1 ≤ n, P x' n_1 := by
      use x, hx
      intro n_1 hn_1
      exact hx_prop n_1 (hn_1.trans hn)
    rw [dif_pos this]
    obtain hy := this.choose_spec
    revert hy
    generalize this.choose = y
    intro hy
    obtain (l|r) := hc.total hx hy.left
    · specialize l N hx_prop
      exact l.left n hn
    · specialize r n hy.right
      exact (r.left n (le_refl n)).symm

lemma exists_max_rel [∀ a, Nonempty (β a)]
    (hP : ∀ (l r : ((a:α) → β a)), ∀ (N:α),
      (∀ n ≤ N, P l n) → (∀ n ≤ N, l n = r n) → ∀ n ≤ N, P r n) :
    ∃ ub : ((a:α) → β a), ∀ l : ((a:α) → β a), rel P ub l → rel P l ub :=
  exists_maximal_of_chains_bounded  (exists_ub P hP) Trans.trans
lemma exists_total_prop [WellFoundedLT α] [∀ a, Nonempty (β a)]
    (hP : ∀ (l r : ((a:α) → β a)), ∀ (N:α),
      (∀ n ≤ N, P l n) → (∀ n ≤ N, l n = r n) → ∀ n ≤ N, P r n)
    (induction_step : ∀ (l : ((a:α) → β a)),∀ (N : α),
      (∀ n < N, P l n) → ∃ r, (rel P l r ∧ (∀ m ≤ N, P r m))):
    ∃ ub : ((a:α) → β a), ∀ n:α, P ub n := by
  obtain ⟨m,hm⟩ := exists_max_rel P hP
  use m
  intro n
  apply wellFounded_lt.induction n
  intro N hN
  specialize induction_step m N hN
  obtain ⟨r,hr⟩ := induction_step
  have hr' : rel P r m := hm r hr.left
  dsimp [rel] at hr hr'
  specialize hr' N
  refine (hr' ?_).right N (le_refl N)
  intro n hn
  exact hr.right n hn

[Edward van de Meent]

out of curiosity, is there a chance that these helper lemmas i suggested are something that have a place in mathlib?

[Edward van de Meent]

i know the proofs likely warrant golfing, but i do think they might be useful to have

[Christopher Hoskin]

@Edward van de Meent thank you very much for your help! I'm traveling today, but will take a look as soon as I get a chance.

The helper lemmas in their current form are the ravings of a desperate man. I think I just need a lemma that lets me commute ∩ and ⋂ and the proof could be quite straight-forward, but I couldn't get Set.inter_iInter to work (without excessive coaxing).

[Christopher Hoskin]

@Edward van de Meent - I meant my helper lemmas from my PR with names like more_confusion and lala2 were ravings - not yours! I hope I haven't inadvertently caused any offence? I'm very grateful for your help and will look at it when I get a moment.

[Edward van de Meent]

ah, it's ok. i'm glad my effort can be of help!

[Edward van de Meent]

for clarity, the helper lemmas i tried to refer to in my earlier question are the ones in the code i posted.