Holder Spaces

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Let $U\subset \mathbb{R}^n$ be an open set. Let $k$ be a positive integer and $0<\gamma\leq 1$. Let $C^{k,\gamma}(U)$ be the set of k times continuously differentiable functions such that $D^ku$ is Hölder continuous with exponent $\gamma$ defined on $U$. I didn't see a proof that $C^{k,\gamma}(U)$ forms a Banach space in mathlib. I want to make a PR about this, and I want to confirm nobody is formalizing this right now before I proceed.

[Yongxi Lin (Aaron)]

The proof relies on the Arzela-Ascoli theorem, which we do have in Mathlib: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.html#BoundedContinuousFunction.arzela_ascoli

[Michael Rothgang]

@Yury G. Kudryashov and I started formalising Moreira's generalisation of the Morse-Sard theorem. The analytical set-up is about $C^{k+(\alpha)}$ functions, for $k$ an integer and $\alpha\in(0,1]$ (English definition, Lean version). This generalises $C^{k,\alpha}$ maps --- so it would be nice to prove e.g. most estimates about Holder functions for this more general class.

[Michael Rothgang]

The blueprint I linked above has proof sketches for all of them; if you want to prove the inverse function theorem, you use the Faa die Bruno formula (which is already in mathlib).

[Michael Rothgang]

So, it could be nice to keep this more general set-up in mind when proving C^k,\alpha is Banach.

[Michael Rothgang]

At the same time, Yury and I got both too busy to finish the project for now, so it'll take some time to get completed. (I still care about finishing it! I just can't be everywhere at once.) So, you shouldn't wait on that project --- but being compatible with these changes would be nice.

[Yongxi Lin (Aaron)]

@Michael Rothgang Thank you for your comments! I would definitely consider this generalization. Just to check I understand the definition of $C^{k+(\alpha)}$ correctly: a $C^{k,\alpha}$ function on $U$ is $C^{k+(\alpha)}$ on the pair $(U,U)$ (Edit: never mind I think you mentioned this in Lemma 5).

[Wuyang]

Proving $C^{k, \gamma}(U)$ is Banach would be a great addition to mathlib, especially if it aligns with the $C^{k+(\alpha)}$ framework for future compatibility.

You might also explore related formalizations in LeanFinder (www.leanfinder.org) to build on existing work.

[Wuyang]

@leanfinder Banach space proof for Hölder space $C^{k, \gamma}(U)$ and relation to $C^{k+(\alpha)}$ generalization in Lean mathlib.

[leanfinder]

Here’s what I found:

• theorem hasFTaylorSeriesUpToOn_top_iff_add (hN : ∞ ≤ N) (k : ℕ) : HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn (n + k : ℕ) f p s := by constructor · intro H n apply H.of_le (natCast_le_of_coe_top_le_withTop hN _) · intro H constructor · exact (H 0).zero_eq · intro m _ apply (H m.succ).fderivWithin m (by norm_cast; omega) · intro m _ apply (H m).cont m (by simp) "For a function $f : E \to F$ between normed spaces over a nontrivially normed field $\mathbb{K}$, a formal multilinear series $p$, a set $s \subseteq E$, and a natural number $k$, the following are equivalent when $N = \infty$:

• The series $p$ is a Taylor series for $f$ up to order $N$ on $s$.

• For every natural number $n$, the series $p$ is a Taylor series for $f$ up to order $n + k$ on $s$." (score: 0.671)
• theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt' (hn : n ≠ ∞) : ContDiffWithinAt 𝕜 (n + 1) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f' : E → E →L[𝕜] F, (∀ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt 𝕜 n f' s x := by refine ⟨fun hf => ?_, ?_⟩ · obtain ⟨u, hu, f_an, f', huf', hf'⟩ := (contDiffWithinAt_succ_iff_hasFDerivWithinAt hn).mp hf obtain ⟨w, hw, hxw, hwu⟩ := mem_nhdsWithin.mp hu rw [inter_comm] at hwu refine ⟨insert x s ∩ w, inter_mem_nhdsWithin _ (hw.mem_nhds hxw), inter_subset_left, ?_, f', fun y hy => ?_, ?_⟩ · intro h apply (f_an h).mono hwu · refine ((huf' y <| hwu hy).mono hwu).mono_of_mem_nhdsWithin ?_ refine mem_of_superset ?_ (inter_subset_inter_left _ (subset_insert _ _)) exact inter_mem_nhdsWithin _ (hw.mem_nhds hy.2) · exact hf'.mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu) · rw [← contDiffWithinAt_insert, contDiffWithinAt_succ_iff_hasFDerivWithinAt hn, insert_eq_of_mem (mem_insert _ _)] rintro ⟨u, hu, hus, f_an, f', huf', hf'⟩ exact ⟨u, hu, f_an, f', fun y hy => (huf' y hy).insert'.mono hus, hf'.insert.mono hus⟩ "Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a set, $x \in E$ a point, and $n \neq \infty$ an extended natural number. Then the following are equivalent:

1. The function $f : E \to F$ is $C^{n+1}$ within $s$ at $x$.

2. There exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ such that:

   • $u \subseteq s \cup \{x\}$,
   • If $n = \omega$, then $f$ is analytic on $u$,
   • There exists a derivative function $$f' : E \to (E \toL[\mathbb{K}] F)$$ such that:
     • For all $y \in u$, $f$ has Fréchet derivative $f'(y)$ within $s$ at $y$,
     • $f'$ is $C^n$ within $s$ at $x$." (score: 0.664)
   • theorem HolderWith.comp_holderOnWith {Cg rg : ℝ≥0} {g : Y → Z} (hg : HolderWith Cg rg g) {Cf rf : ℝ≥0} {f : X → Y} {s : Set X} (hf : HolderOnWith Cf rf f s) : HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s := (hg.holderOnWith univ).comp hf fun _ _ => trivial "Let $X, Y, Z$ be extended pseudo-metric spaces, $s \subseteq X$, and $f : X \to Y$, $g : Y \to Z$ functions. If:

3. $g$ is Hölder continuous on $Y$ with constant $C_g$ and exponent $r_g$,

4. $f$ is Hölder continuous on $s$ with constant $C_f$ and exponent $r_f$,

then the composition $g \circ f$ is Hölder continuous on $s$ with constant $C_g \cdot C_f^{r_g}$ and exponent $r_g \cdot r_f$." (score: 0.662)

• theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt (hn : n ≠ ∞) : ContDiffWithinAt 𝕜 (n + 1) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f' : E → E →L[𝕜] F, (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x := by have h'n : n + 1 ≠ ∞ := by simpa using hn constructor · intro h rcases (contDiffWithinAt_iff_of_ne_infty h'n).1 h with ⟨u, hu, p, Hp, H'p⟩ refine ⟨u, hu, ?_, fun y => (continuousMultilinearCurryFin1 𝕜 E F) (p y 1), fun y hy => Hp.hasFDerivWithinAt le_add_self hy, ?_⟩ · rintro rfl exact Hp.analyticOn (H'p rfl 0) apply (contDiffWithinAt_iff_of_ne_infty hn).2 refine ⟨u, ?_, fun y : E => (p y).shift, ?_⟩ · -- Porting note: without the explicit argument Lean is not sure of the type. convert @self_mem_nhdsWithin _ _ x u have : x ∈ insert x s := by simp exact insert_eq_of_mem (mem_of_mem_nhdsWithin this hu) · rw [hasFTaylorSeriesUpToOn_succ_iff_right] at Hp refine ⟨Hp.2.2, ?_⟩ rintro rfl i change AnalyticOn 𝕜 (fun x ↦ (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn ?_ (Set.mapsTo_univ _ _) exact H'p rfl _ · rintro ⟨u, hu, hf, f', f'_eq_deriv, Hf'⟩ rw [contDiffWithinAt_iff_of_ne_infty h'n] rcases (contDiffWithinAt_iff_of_ne_infty hn).1 Hf' with ⟨v, hv, p', Hp', p'_an⟩ refine ⟨v ∩ u, ?_, fun x => (p' x).unshift (f x), ?_, ?_⟩ · apply Filter.inter_mem _ hu apply nhdsWithin_le_of_mem hu exact nhdsWithin_mono _ (subset_insert x u) hv · rw [hasFTaylorSeriesUpToOn_succ_iff_right] refine ⟨fun y _ => rfl, fun y hy => ?_, ?_⟩ · change HasFDerivWithinAt (fun z => (continuousMultilinearCurryFin0 𝕜 E F).symm (f z)) (FormalMultilinearSeries.unshift (p' y) (f y) 1).curryLeft (v ∩ u) y -- Porting note: needed erw here. -- https://github.com/leanprover-community/mathlib4/issues/5164 erw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'] convert (f'_eq_deriv y hy.2).mono inter_subset_right rw [← Hp'.zero_eq y hy.1] ext z change ((p' y 0) (init (@cons 0 (fun _ => E) z 0))) (@cons 0 (fun _ => E) z 0 (last 0)) = ((p' y 0) 0) z congr norm_num [eq_iff_true_of_subsingleton] · convert (Hp'.mono inter_subset_left).congr fun x hx => Hp'.zero_eq x hx.1 using 1 · ext x y change p' x 0 (init (@snoc 0 (fun _ : Fin 1 => E) 0 y)) y = p' x 0 0 y rw [init_snoc] · ext x k v y change p' x k (init (@snoc k (fun _ : Fin k.succ => E) v y)) (@snoc k (fun _ : Fin k.succ => E) v y (last k)) = p' x k v y rw [snoc_last, init_snoc] · intro h i simp only [WithTop.add_eq_top, WithTop.one_ne_top, or_false] at h match i with | 0 => simp only [FormalMultilinearSeries.unshift] apply AnalyticOnNhd.comp_analyticOn _ ((hf h).mono inter_subset_right) (Set.mapsTo_univ _ _) exact LinearIsometryEquiv.analyticOnNhd _ _ | i + 1 => simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one] apply AnalyticOnNhd.comp_analyticOn _ ((p'_an h i).mono inter_subset_left) (Set.mapsTo_univ _ _) exact LinearIsometryEquiv.analyticOnNhd _ _ "Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a set, $x \in E$ a point, and $n \neq \infty$ an extended natural number. Then the following are equivalent:

1. The function $f : E \to F$ is $C^{n+1}$ within $s$ at $x$.

2. There exists a neighborhood $u$ of $x$ in $s \cup \{x\}$ such that:

   • If $n = \omega$, then $f$ is analytic on $u$.
   • There exists a derivative function $$f' : E \to (E \toL[\mathbb{K}] F)$$ such that:
     • For all $y \in u$, $f$ has Fréchet derivative $f'(y)$ within $u$ at $y$.
     • $f'$ is $C^n$ within $u$ at $x$." (score: 0.662)
   • theorem HolderOnWith.comp_holderWith {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf rf : ℝ≥0} {f : X → Y} (hf : HolderWith Cf rf f) (ht : ∀ x, f x ∈ t) : HolderWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) := holderOnWith_univ.mp <| hg.comp (hf.holderOnWith univ) fun x _ => ht x "Let $X, Y, Z$ be extended pseudo-metric spaces, $t \subseteq Y$, and $f : X \to Y$, $g : Y \to Z$ functions. If:

3. $g$ is Hölder continuous on $t$ with constant $C_g$ and exponent $r_g$

4. $f$ is Hölder continuous on all of $X$ with constant $C_f$ and exponent $r_f$
5. $f$ maps into $t$ (i.e., $f(x) \in t$ for all $x \in X$)

then the composition $g \circ f$ is Hölder continuous on $X$ with constant $C_g \cdot C_f^{r_g}$ and exponent $r_g \cdot r_f$." (score: 0.661)

• theorem HolderOnWith.comp {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf rf : ℝ≥0} {f : X → Y} (hf : HolderOnWith Cf rf f s) (hst : MapsTo f s t) : HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s := by intro x hx y hy rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc, ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg] exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy) "Let $X, Y, Z$ be extended pseudo-metric spaces, $s \subseteq X$, $t \subseteq Y$, and $f : X \to Y$, $g : Y \to Z$ functions. If:

1. $g$ is Hölder continuous on $t$ with constant $C_g$ and exponent $r_g$
2. $f$ is Hölder continuous on $s$ with constant $C_f$ and exponent $r_f$
3. $f$ maps $s$ into $t$ ($f(s) \subseteq t$)

then the composition $g \circ f$ is Hölder co
[message truncated]