two very similiar theorems but only one is working

Stream: new members

[Michael Novak]

I have the following proof that I'm working on:

--Auxilary ψ is continuousely differentiable on I
lemma revParamTransform_contDiffOn_aux (once_diff : 1 ≤ r) (ht₀ : t₀ ∈ I)
  (hc : ContDiffOn ℝ r c I) (hI : IsOpen I) : ContDiffOn ℝ 1 ψ I := by
  apply (contDiffOn_iff_continuousOn_differentiableOn_deriv hI.uniqueDiffOn).mpr
  constructor
  · intro m hm
    have h'm : m=0 ∨ m=1 := by sorry
    rcases h'm with h'm | h'm
    · rw [h'm]
      rw [iteratedDerivWithin_zero]
      exact revParamTransform_continuousOn_aux c I t₀ once_diff ht₀ hc hI
    · rw [h'm]
      rw [iteratedDerivWithin_one]
    sorry

And for some reason, when I use the thorem iteratedDerivWithin_zero it works, but when I use the theorem iteratedDerivWithin_one it doesn't work - lean doesn't recognize the pattern, even though the only difference between the two cases as far as I can see is that in first we have 0 and in the second we have 1. Do you have any idea what could be the reason for that?

[Michael Novak]

This is the error that I get:
Tactic `rewrite` failed: Did not find an occurrence of the pattern iteratedDerivWithin 1 ?m.119 ?m.120 ?m.121 in the target expression ContinuousOn (iteratedDerivWithin 1 ψ I) I

[Vlad Tsyrklevich]

This snippet doesn't compile.

[Michael Novak]

Here is all the previous code:

import Mathlib

open MeasureTheory intervalIntegral

/-- This is a version of the first part of FTC for a function which is continuous on an interval.
    Credit to Aaron Liu. -/
theorem derivWithin_integral_of_continuousOn_interval {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ}
  (h : ContinuousOn f I) (x₀ x : ℝ) (hx₀ : x₀ ∈ I) (hx : x ∈ I) :
  HasDerivWithinAt (fun t ↦  ∫ τ in x₀..t, f τ) (f x) I x :=
  have : intervalIntegral.FTCFilter x (nhdsWithin x I) (nhdsWithin x I) := by
    refine @intervalIntegral.FTCFilter.mk x (nhdsWithin x I) (nhdsWithin x I) ⟨?_⟩ ?_ ?_ ?_
    · rw [Filter.tendsto_smallSets_iff]
      intro t ht
      rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at ht
      obtain ⟨u, hu, hut⟩ := ht
      obtain ⟨a, b, haxb, habx, habu⟩ := exists_Icc_mem_subset_of_mem_nhds hu
      have hab : Set.Icc a b ∩ I ∈ nhdsWithin x I :=
        Set.inter_comm _ _ ▸ inter_mem_nhdsWithin I habx
      filter_upwards [Filter.prod_mem_prod hab hab] with (i, j) ⟨hi, hj⟩
      refine subset_trans (Set.subset_inter ?_ ?_) hut
      · refine subset_trans ?_ habu
        intro k hk
        exact ⟨hi.1.1.trans hk.1.le, hk.2.trans hj.1.2⟩
      · intro k hk
        exact Set.Icc_subset I hi.2 hj.2 (Set.Ioc_subset_Icc_self hk)
    · exact pure_le_nhdsWithin hx
    · exact nhdsWithin_le_nhds
    · exact @Filter.inf_isMeasurablyGenerated _ _ _ _ _
        (Set.OrdConnected.measurableSet ‹_›).principal_isMeasurablyGenerated
  intervalIntegral.integral_hasDerivWithinAt_right
    ((h.mono (Set.OrdConnected.uIcc_subset ‹_› hx₀ hx)).intervalIntegrable)
    (h.stronglyMeasurableAtFilter_nhdsWithin (Set.OrdConnected.measurableSet ‹_›) x)
    (h.continuousWithinAt hx)

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def arclengthParamTransformAux (t₀ : ℝ): ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransform (t₀ : ℝ) :=
  letI ψ := arclengthParamTransformAux c t₀
  ψ.invFun

--Unit speed / arclength reparametrization of a parametrized curve
def arclengthReparamFrom (t₀ : ℝ) : ℝ → E :=
  letI φ := arclengthParamTransform c t₀
  c ∘ φ

-- We now also assume c is a parametrized curve of class Cʳ from the interval I, r≥1.
variable (I : Set ℝ) [I.OrdConnected] (hI : IsOpen I) {r : WithTop ℕ∞}
  (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I) (t₀ : ℝ) (ht₀ : t₀ ∈ I)

--Auxilary definition, so we don't have to type the full long expression everytime
local notation "ψ" => arclengthParamTransformAux c t₀

-- The 'speed' function of a parametrized curve is continuous
lemma speed_continuousOn (hI : IsOpen I) (hc : ContDiffOn ℝ r c I) (once_diff : 1 ≤ r) :
    ContinuousOn (fun t ↦ ‖deriv c t‖) I :=
  Continuous.comp_continuousOn' continuous_norm (hc.continuousOn_deriv_of_isOpen hI once_diff)

/-- An auxiliary lemma giving us the derivitive of ψ on I. -/
lemma revParamTransform_deriv_eq_aux (t : ℝ) (ht : t ∈ I) (once_diff : 1 ≤ r) (ht₀ : t₀ ∈ I)
  (hc : ContDiffOn ℝ r c I) (hI : IsOpen I) : HasDerivWithinAt ψ ‖deriv c t‖ I t := by
  unfold arclengthParamTransformAux
  exact derivWithin_integral_of_continuousOn_interval
    (speed_continuousOn c I hI hc once_diff) t₀ t ht₀ ht

--Auxilary lemma - ψ is continuous
lemma revParamTransform_continuousOn_aux (once_diff : 1 ≤ r) (ht₀ : t₀ ∈ I)
  (hc : ContDiffOn ℝ r c I) (hI : IsOpen I) : ContinuousOn ψ I :=
  fun t ↦ fun ht ↦
    (revParamTransform_deriv_eq_aux c I t₀ t ht once_diff ht₀ hc hI).continuousWithinAt

--Auxilary ψ is continuousely differentiable on I
lemma revParamTransform_contDiffOn_aux (once_diff : 1 ≤ r) (ht₀ : t₀ ∈ I)
  (hc : ContDiffOn ℝ r c I) (hI : IsOpen I) : ContDiffOn ℝ 1 ψ I := by
  apply (contDiffOn_iff_continuousOn_differentiableOn_deriv hI.uniqueDiffOn).mpr
  constructor
  · intro m hm
    have h'm : m=0 ∨ m=1 := by sorry
    rcases h'm with h'm | h'm
    · rw [h'm]
      rw [iteratedDerivWithin_zero]
      exact revParamTransform_continuousOn_aux c I t₀ once_diff ht₀ hc hI
    · rw [h'm]
      rw [iteratedDerivWithin_one]

[Vlad Tsyrklevich]

The rewrite works fine on live lean?

[Michael Novak]

what is live lean?

[Vlad Tsyrklevich]

place your mouse over the code snippet and click the top right most button

[Michael Novak]

I'm using nvim, is it possible to do it with nvim? If not I could try to open the file in vscode.

[Michael Novak]

Vlad Tsyrklevich said:

place your mouse over the code snippet and click the top right most button

And when you say the code snippet do you mean the last rw line?

[Vlad Tsyrklevich]

no, place your mouse over the code box in the browser. Look at the top right, it gives a link to open your code in the live editor

[Michael Novak]

do you mean in vscode?

[Vlad Tsyrklevich]

No, I mean in the browser in Zulip. Here's the link

[Michael Novak]

Vlad Tsyrklevich said:

No, I mean in the browser in Zulip. Here's the link

Oh, I'm sorry, thank you very, I didn't know that this exists

[Michael Novak]

It says that there is an error in the line before the last line (line 89) : · rw [h'm] , although in my computer there isn't such an error. I also can't see what the error says exactly, probably because I'm used to a different editor, it's a bit confusing.

[Michael Novak]

Although it also seems like the last rw (in line 90) did work, even though there is an error sign in the previous line. Very weird.

[Vlad Tsyrklevich]

If you put your cursor over the red squiggles it says "unsolved goal", e.g. it's just highlighting that that arm of the case statement does not have a completed proof.

[Michael Novak]

Oh, right. Thank you very much! The question remains why do I get the error in my computer? Could it be that I need to update the version of Mathlib or, maybe something else?

[Michael Novak]

I tried to change the Mathlib version in the live lean editor to Mathlib v4.24.0 and then I get the same error that I get on my computer. So it does seem like this is related to the Mathlib version.

[Michael Rothgang]

Which mathlib version is your computer using?

[Michael Novak]

O.k. I did lake update in my project directory and it solved the problem. I don't know which version I'm using but I can check it if you know which command to type (if it's still relevant).

[Michael Rothgang]

Great that it's solved! For future reference, looking at lean-toolchain tells you the Lean version you're using.

[Michael Novak]

Thanks!