kebekus/nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update lean

Browse Source
This commit is contained in:
Stefan Kebekus
2024-09-09 06:50:28 +02:00
parent 2ec1335521
commit 1ccc9679e5
3 changed files with 11 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
Nevanlinna/partialDeriv.lean
View File

@@ -297,7 +297,7 @@ lemma partialDeriv_fderivOn
rw [fderiv_clm_apply]
· simp
· convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 hf).2
· simp
@@ -407,7 +407,7 @@ theorem partialDeriv_comm
let f'' := (fderiv ℝ f' z)
have h₁ : HasFDerivAt f' f'' z := by
apply DifferentiableAt.hasFDerivAt
apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)
apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Preorder.le_refl 1)
apply second_derivative_symmetric h₀ h₁ v₁ v₂
@@ -441,7 +441,7 @@ theorem partialDeriv_commOn
have h₁ : HasFDerivAt f' f'' z := by
apply DifferentiableAt.hasFDerivAt
apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2
have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by