Error with rewrite

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I have the following theorem:

theorem abs_conv_implies_summable {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  [CompleteSpace X] (f: ℕ → X): conv_abs_serie 𝕂 f → Summable f := by
    intro fconvabs
    apply abssum_implies_sum 𝕂
    rw [cauchyabssum_iff_abssummable, cauchysum_normed ℝ]
    rw [convabsserie_iff_cauchyabsserie, cauchy_serie_normed ℝ] at fconvabs
    intro ε εpos
    rcases fconvabs ε εpos with ⟨n₀, eq⟩
    use Finset.Icc 0 n₀
    intro F Fneint
    simp only [Real.norm_of_nonneg (Finset.sum_nonneg (fun i x ↦ norm_nonneg (f i)))] at *
    by_cases h: F.Nonempty
    · calc
        ∑ i ∈ F, ‖f i‖ ≤ ∑ i ∈ Finset.Ioc n₀ (Finset.max' F h), ‖f i‖ := by
          apply Finset.sum_le_sum_of_subset_of_nonneg
          · intro n ninF
            rw [Finset.mem_Ioc]
            constructor
            · by_contra! nlen₀
              have: n ∈ Finset.Icc 0 n₀ ∩ F := by
                rw [Finset.mem_inter, Finset.mem_Icc]
                exact And.intro (And.intro (Nat.zero_le n) nlen₀) ninF
              sorry
            · exact Finset.le_max' F n ninF
          · intro i _ _
            exact norm_nonneg (f i)
        _ < ε := by
          have: n₀ < F.max' h := by
            have: F.max' h ∉ Finset.Icc 0 n₀ := by
              by_contra h'
              have : F.max' h ∈ Finset.Icc 0 n₀ ∩ F := by
                exact Finset.mem_inter_of_mem h' (Finset.max'_mem F h)
              sorry
            rw [Finset.mem_Icc] at this
            push_neg at this
            exact this (zero_le (F.max' h))
          exact eq n₀ (F.max' h) (le_refl n₀) (le_of_lt this)
    · rw [Finset.not_nonempty_iff_eq_empty] at h
      rw [h, Finset.sum_empty]
      exact εpos

If it is important to know the details of the definitions I'm using I can provide more detail, but the point is the following.

The sorry in the proof can be sustituted by rw [Fneint] at this followed by the tactic contradiction. However, when doing it I get the following error:

image.png

However, at the point of the proof showed in the next image

image.png

I have some assumptions and If I put them all as the assumptions for a new theorem, the exact same proof but changing the sorry as I've said before works:

lemma aux {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  [CompleteSpace X] {f: ℕ → X} {F: Finset ℕ} {n₀: ℕ} {ε: ℝ} (εpos: 0 < ε)
  (eq: ∀ (n m : ℕ), n₀ ≤ n → n ≤ m → ∑ i ∈ Finset.Ioc n m, ‖f i‖ < ε)
  (Fneint: Finset.Icc 0 n₀ ∩ F = ∅):  ∑ i ∈ F, ‖f i‖ < ε := by
    by_cases h: F.Nonempty
    · calc
        ∑ i ∈ F, ‖f i‖ ≤ ∑ i ∈ Finset.Ioc n₀ (Finset.max' F h), ‖f i‖ := by
          apply Finset.sum_le_sum_of_subset_of_nonneg
          · intro n ninF
            rw [Finset.mem_Ioc]
            constructor
            · by_contra! nlen₀
              have: n ∈ Finset.Icc 0 n₀ ∩ F := by
                rw [Finset.mem_inter, Finset.mem_Icc]
                exact And.intro (And.intro (Nat.zero_le n) nlen₀) ninF
              rw [Fneint] at this
              contradiction
            · exact Finset.le_max' F n ninF
          · intro i _ _
            exact norm_nonneg (f i)
        _ < ε := by
          have: n₀ < F.max' h := by
            have: F.max' h ∉ Finset.Icc 0 n₀ := by
              by_contra h'
              have : F.max' h ∈ Finset.Icc 0 n₀ ∩ F := by
                exact Finset.mem_inter_of_mem h' (Finset.max'_mem F h)
              rw [Fneint] at this
              contradiction
            rw [Finset.mem_Icc] at this
            push_neg at this
            exact this (zero_le (F.max' h))
          exact eq n₀ (F.max' h) (le_refl n₀) (le_of_lt this)
    · rw [Finset.not_nonempty_iff_eq_empty] at h
      rw [h, Finset.sum_empty]
      exact εpos

What's happening here? How can I end my proof?

Thanks in advance for any help.

[Kevin Buzzard]

Nobody can run your code without extra effort, because you didn't make a #mwe . Can you make that effort yourself? In other words, can you edit your original post adding all imports/opens etc so that someone can just click on the "view in Lean 4 playground" link and it will just work? Right now we just get a sea of errors.

[Esteban Martínez Vañó]

Of course, sorry. Here it is:

mwe.lean

I didn't include it because I thought it was a "silly error" and, as you can see, there was a lot to include.

Anyway, this is the GitHub link to the project if it is useful:

https://github.com/Eparoh/Functional_Analysis

[Esteban Martínez Vañó]

By the way, I've included the .lean file because the link to the Lean 4 Web was too long, how can I shorten it?

[Ruben Van de Velde]

Please post it between backticks, not as an attachment

[Esteban Martínez Vañó]

Ruben Van de Velde ha dicho:

Please post it between backticks, not as an attachment

Could you please provide an example of how I should post it? I'll edit it then, but I'm not sure how to do it.

[Esteban Martínez Vañó]

Because the link is so long it does not fit in one post

[Esteban Martínez Vañó]

I've managed to shorten it, but I don't know if it is a valid way to post it:

https://dub.sh/iidUiCl

[Ruben Van de Velde]

import Mathlib

example : True := trivial

[Esteban Martínez Vañó]

But it is a long code. I'll change all non-relevant proofs with sorry and I'll post it that way

[Esteban Martínez Vañó]

Okay, I've shorten it that way. Let's see if now it is okay:

import Mathlib.Analysis.RCLike.Basic
import Mathlib.Topology.Instances.Real
import Mathlib.Topology.UniformSpace.Cauchy
import Mathlib.Topology.Algebra.InfiniteSum.Defs

noncomputable section

open Set Filter Topology Classical Function

class DirectedSet (D: Type*) extends Preorder D, Inhabited D, IsDirected D (fun d d' ↦ d ≤ d')

instance LinearOrder.instDirectedSet {X : Type*} [LinearOrder X] [Inhabited X] : DirectedSet X where
  directed := by
    intro d e
    use max d e
    exact And.intro (le_max_left d e) (le_max_right d e)

instance DirectedSet.instFiniteSubsets {X: Type*}: DirectedSet (Finset X) where
  default := ∅
  directed := by
    intro E F
    use E ∪ F
    constructor
    · exact Finset.subset_union_left
    · exact Finset.subset_union_right

def Limit {X D: Type*} [TopologicalSpace X] [DirectedSet D] (s : D → X) (x: X) : Prop :=
  ∀ U ∈ nhds x, ∃ (d₀ : D), ∀ (d : D), d₀ ≤ d → s d ∈ U

def conv_serie_to {X: Type*} [AddCommMonoid X] [TopologicalSpace X] (f: ℕ → X) (x: X): Prop :=
   Limit (fun (N: ℕ) ↦ ∑ n ≤ N, f n) x

def conv_abs_serie_to {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
   (f: ℕ → X) (t: ℝ) : Prop :=
      conv_serie_to (fun (n: ℕ) ↦ ‖f n‖) t

def conv_abs_serie {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  (f: ℕ → X) : Prop :=
   ∃ (t: ℝ), conv_abs_serie_to 𝕂 f t

def HasSumNet {I X: Type*} [AddCommMonoid X] [TopologicalSpace X] (f: I → X) (x: X): Prop :=
   Limit (fun (E: Finset I) ↦ ∑ e ∈ E, f e) x

def HasAbsSum {I X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
   (f: I → X) (t: ℝ): Prop := HasSumNet (fun (i: I) ↦ ‖f i‖) t

def AbsSummable {I X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
   (f: I → X): Prop := ∃ (t: ℝ), HasAbsSum 𝕂 f t

def CauchyNet {X D: Type*} [DirectedSet D] [UniformSpace X] (s: D → X): Prop :=
   ∀ U ∈ uniformity X, ∃ (d₀: D), ∀ (d e: D), (d₀ ≤ d → d₀ ≤ e → (s d, s e) ∈ U)

def CauchySumNet {I X: Type*} [AddCommMonoid X] [UniformSpace X] (f: I → X): Prop :=
   CauchyNet (fun (E: Finset I) ↦ ∑ e ∈ E, f e)

def CauchySerie {X: Type*} [AddCommMonoid X] [UniformSpace X] (f: ℕ → X): Prop :=
   CauchyNet (fun (N: ℕ) ↦ ∑ n ≤ N, f n)

theorem cauchyabssum_iff_abssummable {I X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  (f: I → X) [CompleteSpace X]: AbsSummable 𝕂 f ↔ CauchySumNet (fun (i: I) ↦ ‖f i‖) := by
    sorry

theorem cauchysum_normed {I X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  (f: I → X):
  CauchySumNet f ↔ ∀ ε, 0 < ε → (∃ (F₀: Finset I), ∀ (F: Finset I), (F₀ ∩ F = ∅ → ‖∑ i ∈ F, f i‖ < ε)) := by
    sorry

theorem cauchy_serie_normed {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  (f: ℕ → X):
  CauchySerie f ↔ ∀ ε, 0 < ε → (∃ (n₀: ℕ), ∀ (n m: ℕ), (n₀ ≤ n → n ≤ m → ‖(∑ i ∈ Finset.Ioc n m, f i)‖ < ε)) := by
    sorry

theorem abssum_implies_sum {I X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  [CompleteSpace X] (f: I → X): AbsSummable 𝕂 f → Summable f := by
    sorry

theorem convabsserie_iff_cauchyabsserie {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  [CompleteSpace X] (f: ℕ → X): conv_abs_serie 𝕂 f ↔ CauchySerie (fun (n: ℕ) ↦ ‖f n‖) := by
    sorry

theorem abs_conv_implies_summable {X: Type*} [SeminormedAddCommGroup X] (𝕂: Type*) [RCLike 𝕂] [NormedSpace 𝕂 X]
  [CompleteSpace X] (f: ℕ → X): conv_abs_serie 𝕂 f → Summable f := by
    intro fconvabs
    apply abssum_implies_sum 𝕂
    rw [cauchyabssum_iff_abssummable, cauchysum_normed ℝ]
    rw [convabsserie_iff_cauchyabsserie, cauchy_serie_normed ℝ] at fconvabs
    intro ε εpos
    rcases fconvabs ε εpos with ⟨n₀, eq⟩
    use Finset.Icc 0 n₀
    intro F Fneint
    simp only [Real.norm_of_nonneg (Finset.sum_nonneg (fun i x ↦ norm_nonneg (f i)))] at *
    by_cases h: F.Nonempty
    · calc
        ∑ i ∈ F, ‖f i‖ ≤ ∑ i ∈ Finset.Ioc n₀ (Finset.max' F h), ‖f i‖ := by
          apply Finset.sum_le_sum_of_subset_of_nonneg
          · intro n ninF
            rw [Finset.mem_Ioc]
            constructor
            · by_contra! nlen₀
              have: n ∈ Finset.Icc 0 n₀ ∩ F := by
                rw [Finset.mem_inter, Finset.mem_Icc]
                exact And.intro (And.intro (Nat.zero_le n) nlen₀) ninF
              sorry
            · exact Finset.le_max' F n ninF
          · intro i _ _
            exact norm_nonneg (f i)
        _ < ε := by
          have: n₀ < F.max' h := by
            have: F.max' h ∉ Finset.Icc 0 n₀ := by
              by_contra h'
              have : F.max' h ∈ Finset.Icc 0 n₀ ∩ F := by
                exact Finset.mem_inter_of_mem h' (Finset.max'_mem F h)
              sorry
            rw [Finset.mem_Icc] at this
            push_neg at this
            exact this (zero_le (F.max' h))
          exact eq n₀ (F.max' h) (le_refl n₀) (le_of_lt this)
    · rw [Finset.not_nonempty_iff_eq_empty] at h
      rw [h, Finset.sum_empty]
      exact εpos

[Etienne Marion]

The issue is with open Classical at the top of the file. The problem is that this will automatically provide instances for things like "the intersection of finite sets exists" but the instance will then clash when the type actually has this instance defined (typically the intersection of Finset Nat has a different instance) so that the intersection you want to rewrite with does not come from the same instance as the one you want to rewrite. I noticed this by writing

have : Finset.Icc 0 n₀ ∩ F = ∅ := Fneint

because the error prints the instance used.

The solution to this problem is simply to remove open Classical (I was advised personally to never write this). Once you do this you get errors. To solve them there are two possibilities: if the statement you write works well and the error only comes in the proof, you can use the tactic classical anywhere you want before the error and it will work. If the statement itself does not work, then you have to add an assumption in the theorem. Typically in your case the theorem cauchysum_normed creates an error because Lean does not know how to synthesize Inter (Finset I) you can solve this by adding [DecidableEq I] to your hypotheses. This is not an issue because when you want to apply cauchysum_normed somewhere you can just use classical before and you won't need to provide the instance.

[Esteban Martínez Vañó]

I see. Thank you!

I'll try then to avoid using open Classical, but then I have some other problems.

Without opening it, how can I make the following definition work?

import Mathlib.Topology.Instances.Real

noncomputable section

class DirectedSet (D: Type*) extends Preorder D, Inhabited D, IsDirected D (fun d d' ↦ d ≤ d')

def default' (D: Type*) [DirectedSet D] := @Inhabited.default D DirectedSet.toInhabited

def seqfromnet {X D: Type*} [PseudoMetricSpace X] [DirectedSet D] (t: D → X) (s: ℕ → ℝ): ℕ → D
  | 0 => if h: ∃ d₀, (∀ (d e : D), d₀ ≤ d → d₀ ≤ e → dist (t d) (t e) < s 0) then Classical.choose h else default' D
  | n + 1 => if h: ∃ (d₀: D), ((seqfromnet t s n) ≤ d₀ ∧ ((∀ (d e : D), d₀ ≤ d → d₀ ≤ e → dist (t d) (t e) < s (n + 1)))) then Classical.choose h else default' D

And also, what does exactly the tactic classical do? It is like opening Classical and all its related theorems, but only for the proof?

[Esteban Martínez Vañó]

I've seen that I can make a section for the definition and put there the open Classical, but is there a better option?

[Etienne Marion]

You can do this for example:

import Mathlib.Topology.Instances.Real

noncomputable section

class DirectedSet (D: Type*) extends Preorder D, Inhabited D, IsDirected D (fun d d' ↦ d ≤ d')

def default' (D: Type*) [DirectedSet D] := @Inhabited.default D DirectedSet.toInhabited

def seqfromnet {X D: Type*} [PseudoMetricSpace X] [DirectedSet D] (t: D → X) (s: ℕ → ℝ): ℕ → D := fun k ↦ by
  classical
  exact match k with
  | 0 => if h: ∃ d₀, (∀ (d e : D), d₀ ≤ d → d₀ ≤ e → dist (t d) (t e) < s 0) then Classical.choose h else default' D
  | n + 1 => if h: ∃ (d₀: D), ((seqfromnet t s n) ≤ d₀ ∧ ((∀ (d e : D), d₀ ≤ d → d₀ ≤ e → dist (t d) (t e) < s (n + 1)))) then Classical.choose h else default' D

Usually you don't want to use tactics in a definition but here it's not a problem because the only tactic used to build the object is exact so it should work in exactly the same way. I do not know if there is a better option.

[Esteban Martínez Vañó]

Okay, that works. Thanks!

Etienne Marion ha dicho:

Usually you don't want to use tactics in a definition but here it's not a problem because the only tactic used to build the object is exact so it should work in exactly the same way. I do not know if there is a better option.

I see. I'll take it into account.

[Kim Morrison]

I would be inclined to just write open Classical in before the def.

Note also you don't need default' at all. Just write default instead of default' D.

[Esteban Martínez Vañó]

Kim Morrison ha dicho:

I would be inclined to just write open Classical in before the def.

I'll also take it into consideration :+1:

Kim Morrison ha dicho:

Note also you don't need default' at all. Just write default instead of default' D.

You are right. In some context I got some errors and that's why I introduce the theorem default' and I've used it since then without thinking about it.