Independence of differentials read in a chart

HasIndependentDifferentialsAt E z a — the linear independence of the manifold derivatives of the z i at a — is the linear independence of the derivatives of the z i ∘ φ⁻¹ at φ a for any chart φ of the maximal atlas at a, hence chart-independent (linearIndependent_fderiv_chart_iff'). hasIndependentDifferentialsAt_iff_chart of Hironaka/Manifold/AdaptedChart.lean proves this for functions differentiable at a; here the hypothesis is removed: a function not differentiable at a has mfderiv = 0 and, read in the chart, fderiv = 0 (differentiability of z i ∘ φ⁻¹ at φ a would make z i differentiable at a), so both families contain 0 and neither is independent. This is the chart form of the independence of differentials of Bierstone–Milman's regular coordinate charts [BM97, (0.3)] and Kollár's local coordinates [Kol07, Definition 73].

theorem Manifold.mdifferentiableAt_of_differentiableAt_comp_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {z : M → 𝕜} (hd : DifferentiableAt 𝕜 (z ∘ ↑φ.symm) (↑φ a)) : MDiffAt z a

A function whose chart reading is differentiable at φ a is MDifferentiableAt a.

theorem Manifold.linearIndependent_fderiv_chart_iff' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {c : ℕ} (z : Fin c → M → 𝕜) : HasIndependentDifferentialsAt E z a ↔ LinearIndependent 𝕜 fun (i : Fin c) => fderiv 𝕜 (z i ∘ ↑φ.symm) (↑φ a)

Independence of the differentials at a is the linear independence of the derivatives read in any chart of the maximal atlas at a ([BM97, (0.3)]; [Kol07, Definition 73]).