Integral currents, geometric homology and minimizing hypersurfaces

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremStokes' theorem for test forms#

the integration current annihilates every exact test form.

Orientation.integrationCurrent_extDerivCLM.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {k : ℕ}
  (o : Orientation ℝ E (Fin (k + 1))) (Ω : TopologicalSpace.Opens E)
  (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] ℝ) ⊤) :
  (o.integrationCurrent Ω) (TestFunction.extDerivCLM ω) = 0
Lean

Formalized in Tau Ceti as Orientation.integrationCurrent_extDerivCLM.

Sources
LeanOrientation.integrationCurrent_extDerivCLM
Uses 2
Statement usesOrientation.integrationCurrent · TestFunction.extDerivCLM

Theoremd ∘ d = 0 on test forms, as an identity of continuous linear maps# 

TestFunction.extDerivCLM_comp_extDerivCLM.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  {Ω : TopologicalSpace.Opens E} {k : ℕ} : TestFunction.extDerivCLM ∘SL TestFunction.extDerivCLM = 0
Lean

Formalized in Tau Ceti as TestFunction.extDerivCLM_comp_extDerivCLM.

Sources
LeanTestFunction.extDerivCLM_comp_extDerivCLM
Uses 1
Statement usesTestFunction.extDerivCLM

TheoremThe derivative of a regularization#

At every admissible translation, the derivative of x ↦ T (ρ (· - x)) in the direction v is the regularization of the distributional derivative ∂_{v} T.

Distribution.fderiv_translatePairing_apply.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  {Ω V : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] (T : Distribution Ω F ⊤)
  (ρ : TestFunction V ℝ ⊤) {x : E} (hx : Set.MapsTo (fun x_1 => x_1 + x) (tsupport ⇑ρ) ↑Ω) (v : E) :
  (fderiv ℝ (T.translatePairing ρ) x) v = (LineDeriv.lineDerivOp v T).translatePairing ρ x
Lean

Formalized in Tau Ceti as Distribution.fderiv_translatePairing_apply.

Sources
LeanDistribution.fderiv_translatePairing_apply
Uses 2 · Used by 3
Proof usesA distribution has finite order on each compact set · Uniform first-order Taylor estimate in a parameter
Used byDistributions with vanishing derivatives have locally constant regularizations · The constancy theorem · The constancy theorem in degree zero

TheoremDistributions with vanishing derivatives have locally constant regularizations#

If every directional derivative of T vanishes, then x ↦ T (ρ (· - x)) is constant on every preconnected open set of translations for which ρ (· - x) is supported in Ω.

Distribution.translatePairing_eq_of_lineDerivOp_eq_zero.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  {Ω V : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] {T : Distribution Ω F ⊤}
  (hT : ∀ (v : E), LineDeriv.lineDerivOp v T = 0) (ρ : TestFunction V ℝ ⊤) {U : Set E}
  (hUo : IsOpen U) (hUc : IsPreconnected U)
  (hU : ∀ x ∈ U, Set.MapsTo (fun x_1 => x_1 + x) (tsupport ⇑ρ) ↑Ω) {x y : E} (hx : x ∈ U)
  (hy : y ∈ U) : T.translatePairing ρ x = T.translatePairing ρ y
Lean

Formalized in Tau Ceti as Distribution.translatePairing_eq_of_lineDerivOp_eq_zero.

Sources
LeanDistribution.translatePairing_eq_of_lineDerivOp_eq_zero
Uses 3 · Used by 2
Proof usesA distribution has finite order on each compact set · The derivative of a regularization · Uniform first-order Taylor estimate in a parameter
Used byThe constancy theorem · The constancy theorem in degree zero

TheoremA distribution has finite order on each compact set#

For a compact K ⊆ Ω there are an order N and a constant C such that ‖T φ‖ ≤ C * M for every test function φ supported in K whose derivatives of order at most N are all bounded by M.

Distribution.exists_norm_apply_le.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E}
  (T : Distribution Ω F ⊤) {K : TopologicalSpace.Compacts E} (hK : ↑K ⊆ ↑Ω) :
  ∃ N C,
    0 ≤ C ∧
      ∀ (φ : TestFunction Ω ℝ ⊤),
        tsupport ⇑φ ⊆ ↑K →
          ∀ (M : ℝ), 0 ≤ M → (∀ i ≤ N, ∀ (x : E), ‖iteratedFDeriv ℝ i (⇑φ) x‖ ≤ M) → ‖T φ‖ ≤ C * M
Lean

Formalized in Tau Ceti as Distribution.exists_norm_apply_le.

Sources
LeanDistribution.exists_norm_apply_le
Used by 4
Used byDistributions with vanishing derivatives have locally constant regularizations · The derivative of a regularization · The constancy theorem · The constancy theorem in degree zero

DefinitionOrientation.integrationCurrent#

The oriented integration current [[Ω]] of an open set Ω of an oriented real vector space E of dimension m: the continuous linear functional ω ↦ ∫_Ω ω on test m-forms on Ω. For any basis b of orientation o it is ω ↦ ∫ x, ω x b ∂b.addHaar (Orientation.integrationCurrent_apply). If m is not the dimension of E, it is zero.

Orientation.integrationCurrent.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {m : ℕ} {n : ℕ∞}
  (o : Orientation ℝ E (Fin m)) (Ω : TopologicalSpace.Opens E) :
  TestFunction Ω (E [⋀^Fin m]→L[ℝ] ℝ) n →L[ℝ] ℝ
Lean

Formalized in Tau Ceti as Orientation.integrationCurrent.

Sources
LeanOrientation.integrationCurrent
Used by 4
Used byStokes' theorem for test forms · The constancy theorem · The constancy theorem in degree zero · The local constancy theorem

DefinitionTestFunction.extDerivCLM#

The exterior derivative of test k-forms on Ω with coefficients in F, as a continuous linear map into the test (k + 1)-forms. It is the alternatization ContinuousAlternatingMap.alternatizeUncurryFinCLM of the Fréchet derivative TestFunction.fderivCLM, so pointwise it is Mathlib's extDeriv.

TestFunction.extDerivCLM.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E}
  {k : ℕ} : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤ →L[ℝ] TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤
Lean

Formalized in Tau Ceti as TestFunction.extDerivCLM.

Sources
LeanTestFunction.extDerivCLM
Used by 4
Used byd ∘ d = 0 on test forms, as an identity of continuous linear maps · Stokes' theorem for test forms · The constancy theorem · The local constancy theorem

DefinitionMaps on vector-valued tests are operator-valued distributions#

For a finite-dimensional real normed space F and a real normed space V, the continuous linear maps from the F-valued test functions on Ω to V correspond to the F →L[ℝ] V-valued distributions on Ω: a map T corresponds to the distribution ψ ↦ (v ↦ T (ψ • v)). Both spaces carry the topology of uniform convergence on compact sets, and the correspondence is a homeomorphism for these topologies.

TestFunction.dualEquivDistribution.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V]
  {n : ℕ∞} :
  CompactConvergenceCLM (RingHom.id ℝ) (TestFunction Ω F n) V ≃L[ℝ] Distribution Ω (F →L[ℝ] V) n
Lean

Formalized in Tau Ceti as TestFunction.dualEquivDistribution.

Sources
LeanTestFunction.dualEquivDistribution

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.