OAI/Geometry/EinsteinFour/OperatorGreen.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Averages.weighted_operator_green line 23

   Source documentation

   The first and second derivatives of the varying coefficient contribute exactly the one-half correction. No coefficient is assumed parallel.

   theorem weighted_operator_green
       (φ : ℝ → Ω ≃ᵐ Ω)
       (hφ : Continuous (fun p : ℝ × Ω => φ p.1 p.2))
       (hμ : ∀ t, MeasurePreserving (φ t) μ μ)
       (m dm : C(Ω, ℝ)) (f df ddf : C(Ω, E))
       (A dA ddA : C(Ω, E →L[ℝ] E))
       (hself : ∀ x u v, inner ℝ (dA x u) v = inner ℝ u (dA x v))
       (hm : ∀ t x, HasDerivAt (fun s => m (φ s x)) (dm (φ t x)) t)
       (hf : ∀ t x, HasDerivAt (fun s => f (φ s x)) (df (φ t x)) t)
       (hdf : ∀ t x, HasDerivAt (fun s => df (φ s x)) (ddf (φ t x)) t)
       (hA : ∀ t x, HasDerivAt (fun s => A (φ s x)) (dA (φ t x)) t)
       (hdA : ∀ t x, HasDerivAt (fun s => dA (φ s x)) (ddA (φ t x)) t) :
   …

2. theorem OAI.PositiveEinsteinFour.Averages.weighted_four_operator_green line 83

   Source documentation

   The nonparallel coefficient identity summed over the four tangent directions. The correction retains both its Laplacian and the weight gradient.

   theorem weighted_four_operator_green
       (φ : Fin 4 → ℝ → Ω ≃ᵐ Ω)
       (hφ : ∀ i, Continuous (fun p : ℝ × Ω => φ i p.1 p.2))
       (hμ : ∀ i t, MeasurePreserving (φ i t) μ μ)
       (m : C(Ω, ℝ)) (dm : Fin 4 → C(Ω, ℝ))
       (f : C(Ω, E)) (df ddf : Fin 4 → C(Ω, E))
       (A : C(Ω, E →L[ℝ] E)) (dA ddA : Fin 4 → C(Ω, E →L[ℝ] E))
       (hself : ∀ i x u v, inner ℝ (dA i x u) v = inner ℝ u (dA i x v))
       (hm : ∀ i t x, HasDerivAt (fun s => m (φ i s x)) (dm i (φ i t x)) t)
       (hf : ∀ i t x, HasDerivAt (fun s => f (φ i s x)) (df i (φ i t x)) t)
       (hdf : ∀ i t x, HasDerivAt (fun s => df i (φ i s x)) (ddf i (φ i t x)) t)
       (hA : ∀ i t x, HasDerivAt (fun s => A (φ i s x)) (dA i (φ i t x)) t)
   …

3. theorem OAI.PositiveEinsteinFour.Averages.weighted_scalar_coefficient_green line 131

   Source documentation

   A variable scalar tensor coefficient contributes its divergence term. Summing this identity is the derivative-slot curvature integration step.

   theorem weighted_scalar_coefficient_green
       (φ : ℝ → Ω ≃ᵐ Ω)
       (hφ : Continuous (fun p : ℝ × Ω => φ p.1 p.2))
       (hμ : ∀ t, MeasurePreserving (φ t) μ μ)
       (m dm a da : C(Ω, ℝ)) (f df g dg : C(Ω, E))
       (hm : ∀ t x, HasDerivAt (fun s => m (φ s x)) (dm (φ t x)) t)
       (ha : ∀ t x, HasDerivAt (fun s => a (φ s x)) (da (φ t x)) t)
       (hf : ∀ t x, HasDerivAt (fun s => f (φ s x)) (df (φ t x)) t)
       (hg : ∀ t x, HasDerivAt (fun s => g (φ s x)) (dg (φ t x)) t) :
       (∫ x, m x * a x * inner ℝ (f x) (dg x) +
         dm x * a x * inner ℝ (f x) (g x) ∂μ) =
         -(∫ x, m x * a x * inner ℝ (df x) (g x) ∂μ) -
   …