HaarCurrents.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.KervaireHaarFlow.hasCompactSupport_of_compact line 28
lemma OAI.KervaireHaarFlow.continuous_integrable line 32

lemma OAI.KervaireHaarFlow.hasDerivAt_integral_compact line 37

Source documentation

Compactness supplies the domination needed for differentiation with respect to a real parameter. This lemma only assumes actual joint continuity and actual pointwise derivatives.

lemma hasDerivAt_integral_compact {f df : ℝ → S → E}
    (hf : Continuous (Function.uncurry f)) (hd : Continuous (Function.uncurry df))
    (hfd : ∀ t x, HasDerivAt (fun u ↦ f u x) (df t x) t) (t : ℝ) :
    HasDerivAt (fun u ↦ ∫ x, f u x ∂μ) (∫ x, df t x ∂μ) t := by
…

lemma OAI.KervaireHaarFlow.integral_deriv_eq_zero_of_invariant line 58

Source documentation

The infinitesimal form of invariance under a measure-preserving flow.

lemma integral_deriv_eq_zero_of_invariant {f df : ℝ → S → E}
    (hf : Continuous (Function.uncurry f)) (hd : Continuous (Function.uncurry df))
    (hfd : ∀ t x, HasDerivAt (fun u ↦ f u x) (df t x) t)
    (hinv : ∀ t, (∫ x, f t x ∂μ) = ∫ x, f 0 x ∂μ) (t : ℝ) :
    (∫ x, df t x ∂μ) = 0 := by
…

lemma OAI.KervaireClosedCurrent.contDiff_multilinear_eval line 79

Source documentation

Smoothness of simultaneous evaluation, including a varying multilinear map.

lemma contDiff_multilinear_eval {n : ℕ}
    {f : E → ContinuousMultilinearMap ℝ (fun _ : Fin n ↦ E) F}
    {V : Fin n → E → E} (hf : ContDiff ℝ ∞ f) (hV : ∀ i, ContDiff ℝ ∞ (V i)) :
    ContDiff ℝ ∞ (fun x ↦ f x (V · x)) := by
…

lemma OAI.KervaireClosedCurrent.contDiff_eval_fields line 108

Source documentation

Evaluation of a smooth form on smooth vector fields is smooth.

lemma contDiff_eval_fields {n : ℕ} {form : E → E [⋀^Fin n]→L[ℝ] F}
    {V : Fin n → E → E} (hf : ContDiff ℝ ∞ form) (hV : ∀ i, ContDiff ℝ ∞ (V i)) :
    ContDiff ℝ ∞ (fun x ↦ form x (V · x)) := by
…

lemma OAI.KervaireCurrentHomotopy.integral_eval_constant line 128

Source documentation

A moving-frame homotopy formula for a closed current, proved from the actual exterior derivative identity and differentiation under a compact-parameter integral.

lemma integral_eval_constant {n : ℕ} {e : S → E} (he : Continuous e)
    {form : (ℝ × E) → (ℝ × E) [⋀^Fin (n+1)]→L[ℝ] ℝ}
    (hf : ContDiff ℝ ∞ form)
    {V : Fin (n+2) → (ℝ × E) → (ℝ × E)} (hV : ∀ i, ContDiff ℝ ∞ (V i))
    (hVzero : ∀ p, V 0 p = (1, 0))
    (hdiv : ∀ (t : ℝ) (i : Fin (n+2)), i ≠ 0 → ∀ (g : (ℝ × E) → ℝ),
      ContDiff ℝ ∞ g →
      (∫ x, fderiv ℝ g (t,e x) (V i (t,e x)) ∂μ) = 0)
    (hbracket : ∀ (t : ℝ) (x : S) (i j : Fin (n+1)), i ≤ j →
      form (t,e x) (Matrix.vecCons (lieBracket ℝ (V i.castSucc) (V j.succ) (t,e x))
        (j.removeNth (i.castSucc.removeNth (fun l ↦ V l (t,e x))))) = 0)
    (hclosed : ∀ (t : ℝ) (x : S),
…

def OAI.KervaireHaarFlow.expFlow line 200
Source documentation
The genuine exponential flow in the unitary group.
```
def expFlow (a : skewAdjoint.submodule ℝ B) (t : ℝ) : unitary B :=
…
```
lemma OAI.KervaireHaarFlow.integral_unitary_fderiv_mul_eq_zero line 211
Source documentation
Right-invariant vector fields on a compact unitary group have zero Haar divergence. The derivative is the ambient Fréchet derivative.
```
lemma integral_unitary_fderiv_mul_eq_zero {g : B → ℝ} (hg : ContDiff ℝ ∞ g)
    (a : skewAdjoint.submodule ℝ B) :
    (∫ x : unitary B, fderiv ℝ g (x : B) ((x : B) * a) ∂μ) = 0 := by
…
```
def OAI.KervaireUnitaryHaarCurrent.liftField line 240
Source documentation
The autonomous lift of a right-translation field to the time cylinder.
```
def liftField (a : B) : (ℝ × B) →L[ℝ] (ℝ × B) :=
…
```
lemma OAI.KervaireUnitaryHaarCurrent.liftField_apply line 244
lemma OAI.KervaireUnitaryHaarCurrent.bracket_lift line 246
lemma OAI.KervaireUnitaryHaarCurrent.bracket_time_lift line 252
lemma OAI.KervaireUnitaryHaarCurrent.bracket_lift_time line 256
lemma OAI.KervaireUnitaryHaarCurrent.integral_liftField_eq_zero line 265
lemma OAI.KervaireCompactUnitary.isCompact_unitary line 285
lemma OAI.KervaireCompactUnitary.compactSpace line 293
Source documentation
The unitary group of a finite-dimensional complex C⋆-algebra is compact.
```
lemma compactSpace : CompactSpace (unitary B) :=
…
```