circulatingPart

formal source

  19def gradPart {ι : Type*} (X : NESSVectorField ι) : ι → ℝ :=
  20  fun i => - X.freeEnergyGradient i
  21
  22def circulatingPart {ι : Type*} (X : NESSVectorField ι) : ι → ℝ :=
  23  fun i => X.v i + X.freeEnergyGradient i
  24
  25theorem helmholtz_split {ι : Type*} (X : NESSVectorField ι) :
  26    ∀ i, X.v i = gradPart X i + circulatingPart X i := by
  27  intro i
  28  unfold gradPart circulatingPart
  29  ring
  30
  31def DivergenceFree {ι : Type*} [Fintype ι] (w : ι → ℝ) : Prop :=
  32  ∑ i, w i = 0
  33
  34structure HelmholtzDecompositionCert (ι : Type*) [Fintype ι] where
  35  split : ∀ X : NESSVectorField ι, ∀ i, X.v i = gradPart X i + circulatingPart X i
  36  divergence_free_condition : ∀ X : NESSVectorField ι,
  37    DivergenceFree (circulatingPart X) → ∑ i, circulatingPart X i = 0
  38
  39theorem helmholtzDecompositionCert_holds (ι : Type*) [Fintype ι] :
  40    HelmholtzDecompositionCert ι :=
  41{ split := helmholtz_split
  42  divergence_free_condition := by
  43    intro X h
  44    exact h }
  45
  46end
  47
  48end IndisputableMonolith.Information.HelmholtzDecomposition