CurrentPullback.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.KervaireCurrentPullback.contDiff_of_multilinear line 32
Source documentation
The finite-dimensional alternating-map subspace is split by a continuous linear map. This lets ordinary multilinear calculus establish smooth pullback without a manifold API.
```
lemma contDiff_of_multilinear {n : ℕ} [FiniteDimensional ℝ F] [FiniteDimensional ℝ H]
    {f : E → F [⋀^Fin n]→L[ℝ] H}
    (hf : ContDiff ℝ ∞ (fun x ↦ (f x).toContinuousMultilinearMap)) :
    ContDiff ℝ ∞ f := by
…
```

lemma OAI.KervaireCurrentPullback.contDiff_compLinear line 49

Source documentation

Smoothness of pullback as an operation on smooth forms and smooth differentials.

lemma contDiff_compLinear {n : ℕ} [FiniteDimensional ℝ F] [FiniteDimensional ℝ H]
    {f : E → G [⋀^Fin n]→L[ℝ] H} {g : E → F →L[ℝ] G}
    (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g) :
    ContDiff ℝ ∞ (fun x ↦ (f x).compContinuousLinearMap (g x)) := by
…

lemma OAI.KervaireCurrentPullback.contDiff_pullback line 58

lemma OAI.KervaireCurrentPullback.eval_eq_zero_of_subspace line 65

Source documentation

An alternating form vanishes on more vectors than the dimension of their common subspace.

lemma eval_eq_zero_of_subspace {n : ℕ} (L : Submodule ℝ F) [FiniteDimensional ℝ L]
    (hL : Module.finrank ℝ L < n) (form : F [⋀^Fin n]→L[ℝ] ℝ)
    (v : Fin n → F) (hv : ∀ i, v i ∈ L) : form v = 0 := by
…

lemma OAI.KervaireCurrentPullback.extDeriv_pullback_eval_eq_zero line 77

Source documentation

Pullbacks are closed on frames whose images lie in a subspace of the target dimension.

lemma extDeriv_pullback_eval_eq_zero {n : ℕ} {f : E → F}
    {form : F → F [⋀^Fin n]→L[ℝ] ℝ} (hf : ContDiff ℝ ∞ f) (hform : ContDiff ℝ ∞ form)
    (x : E) (v : Fin (n+1) → E) (L : Submodule ℝ F) [FiniteDimensional ℝ L]
    (hL : Module.finrank ℝ L ≤ n) (hv : ∀ i, fderiv ℝ f x (v i) ∈ L) :
    extDeriv (fun x ↦ (form (f x)).compContinuousLinearMap (fderiv ℝ f x)) x v = 0 := by
…

def OAI.KervaireUnitaryTangent.tangent line 98
Source documentation
The real tangent subspace at a unitary, represented in the ambient algebra.
```
def tangent (u : unitary B) : Submodule ℝ B :=
…
```
lemma OAI.KervaireUnitaryTangent.mem_tangent line 102
lemma OAI.KervaireUnitaryTangent.hasDerivAt_mem_tangent line 109
Source documentation
Differentiating the actual unitary identity gives a tangent vector.
```
lemma hasDerivAt_mem_tangent {f : ℝ → B} {d : B} {t : ℝ}
    (hd : HasDerivAt f d t) (hf : ∀ s, f s ∈ unitary B) :
    d ∈ tangent ⟨f t, hf t⟩ := by
…
```
Mentions: OAI.KervaireUnitaryTangent.tangent
lemma OAI.KervaireUnitaryTangent.finrank_tangent_le line 124

lemma OAI.KervaireUnitaryTangent.fderiv_mem_tangent line 129

Source documentation

A Fréchet differential is tangent along any genuine unitary curve.

lemma fderiv_mem_tangent {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {f : E → B} {x v : E} (hf : DifferentiableAt ℝ f x)
    (c : ℝ → E) (hc : c 0 = x) (hd : HasDerivAt c v 0)
    (hu : ∀ t, f (c t) ∈ unitary B) :
    fderiv ℝ f x v ∈ tangent ⟨f x, hc ▸ hu 0⟩ := by
…

Mentions: OAI.KervaireUnitaryTangent.tangent

lemma OAI.KervaireAlternatingSpan.eval_cons_eq_zero line 144
lemma OAI.KervaireAlternatingSpan.basis_mem_span_except_two line 151
lemma OAI.KervaireAlternatingSpan.removeNth_removeNth_range line 166
lemma OAI.KervaireAlternatingSpan.eval_bracket_eq_zero line 187
lemma OAI.KervaireHorizontalCurrent.time_tangent line 219
lemma OAI.KervaireHorizontalCurrent.horizontal_tangent line 230

lemma OAI.KervaireHorizontalCurrent.integral_pullback_constant line 243

Source documentation

Haar current homotopy invariance in a horizontal frame. The bracket condition is an explicit infinitesimal condition (not a topological-degree assumption).

lemma integral_pullback_constant {n : ℕ} (a : Fin (n+1) → skewAdjoint.submodule ℝ B)
    {f : (ℝ × B) → C} (hf : ContDiff ℝ ∞ f)
    (hu : ∀ t (x : unitary B), f (t,(x : B)) ∈ unitary C)
    (hdim : Module.finrank ℝ (skewAdjoint.submodule ℝ C) ≤ n+1)
    (hbr : ∀ t (x : unitary B) (i j : Fin (n+1)), i ≠ j →
      ∃ c : Fin (n+1) → ℝ, c i = 0 ∧ c j = 0 ∧
        fderiv ℝ f (t,(x : B)) (0,(x : B)*((a i : B)*(a j : B)-(a j : B)*(a i : B))) =
          ∑ l, c l • fderiv ℝ f (t,(x : B)) (0,(x : B)*(a l : B)))
    (form : C → C [⋀^Fin (n+1)]→L[ℝ] ℝ) (hform : ContDiff ℝ ∞ form) (t₀ t₁ : ℝ) :
    (∫ x : unitary B, form (f (t₀,(x : B)))
        (fun i ↦ fderiv ℝ f (t₀,(x : B)) (0,(x : B)*(a i : B))) ∂μ) =
    (∫ x : unitary B, form (f (t₁,(x : B)))
…