Linear combinations

-- Generated by scripts/release04/gen_platform_tree.py (ATLAS-RELEASE-04) by skeleton subtraction from Atlas/EinsteinMaxwell/Variation/Local.lean
-- definition bundle: kept ExactVacuumAtlas.Variation.lcomb
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Variation_Defs
/-! # Locality and linearity of the explicit first-variation operators (ATLAS-IV-03)

* Locality (`*_congr`): on an open set `V`, the operators only depend on the background `(g, ginv, F)`
  and the perturbation `(h, f)` on `V` (every coordinate derivative is local, `pd_congr_of_eqOn`).
* Linearity on the admissible class (open `U`, background and perturbations `C^∞` on `U`, order `∞`):
  `linEinstein`, `linMaxwell`, `linFaraday` of `lcomb c₁ h₁ c₂ h₂`, `lcomb c₁ f₁ c₂ f₂` are the same real
  linear combinations of the values (`*_lcomb`); additivity (`*_add`) and real homogeneity (`*_smul`) are
  the special cases. Perturbations are arbitrary `C^∞` functions of all four coordinates (no symmetry,
  stationarity or analyticity assumption). Stated for the physical dimension `4`. -/

open scoped ContDiff
open ExactVacuumAtlas.EinsteinMaxwell

namespace ExactVacuumAtlas.Variation

/-! ## Locality -/

section congr

variable {n : ℕ} {V : Set (Pt n)} {g g' ginv ginv' h h' : Metric n} {F F' f f' : TwoForm n}

end congr

section congr4

variable {V : Set (Pt 4)} {g g' ginv ginv' h h' : Metric 4} {F F' f f' : TwoForm 4}

end congr4

/-! ## Linearity (4D, admissible `C^∞` class) -/

/-- Real linear combination `c₁ T₁ + c₂ T₂` of two component families (class B notation). -/
def lcomb {n : ℕ} (c₁ : ℝ) (T₁ : Fin n → Fin n → Pt n → ℝ) (c₂ : ℝ) (T₂ : Fin n → Fin n → Pt n → ℝ) :
    Fin n → Fin n → Pt n → ℝ :=
  fun i j y => c₁ * T₁ i j y + c₂ * T₂ i j y

section lin

variable {U : Set (Pt 4)} {g ginv h₁ h₂ : Metric 4} {F f₁ f₂ : TwoForm 4} (c₁ c₂ : ℝ)

variable (hU : IsOpen U) (hg : ∀ i j, ContDiffOn ℝ ∞ (g i j) U) (hgi : ∀ i j, ContDiffOn ℝ ∞ (ginv i j) U)
include hU hg hgi

variable {c₁ c₂} (hh₁ : ∀ i j, ContDiffOn ℝ ∞ (h₁ i j) U) (hh₂ : ∀ i j, ContDiffOn ℝ ∞ (h₂ i j) U)
include hh₁ hh₂

variable (hF : ∀ i j, ContDiffOn ℝ ∞ (F i j) U) (hf₁ : ∀ i j, ContDiffOn ℝ ∞ (f₁ i j) U)
  (hf₂ : ∀ i j, ContDiffOn ℝ ∞ (f₂ i j) U)
include hF

end lin

/-! ### Additivity and homogeneity -/

section addsmul

variable {U : Set (Pt 4)} {g ginv h h₁ h₂ : Metric 4} {F f f₁ f₂ : TwoForm 4}
  (hU : IsOpen U) (hg : ∀ i j, ContDiffOn ℝ ∞ (g i j) U) (hgi : ∀ i j, ContDiffOn ℝ ∞ (ginv i j) U)
include hU hg hgi

variable (hF : ∀ i j, ContDiffOn ℝ ∞ (F i j) U)
include hF

end addsmul

end ExactVacuumAtlas.Variation

• Endorsed by Shuze Chen · Oct 21, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 21, 2026

  Confirmed by the mission captain (proposal self-audit).