OAI/Geometry/EinsteinFour/TraceGreen.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Averages.weighted_trace_green line 21

   Source documentation

   Integrate the trace block against the rough Laplacian. The gradient of its coefficient is retained on the right-hand side.

   theorem weighted_trace_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(Ω, ℝ))
       (B : C(Ω, E)) (dB Z dZ : Fin 4 → C(Ω, E))
       (hm : ∀ i t x, HasDerivAt (fun s => m (φ i s x)) (dm i (φ i t x)) t)
       (hB : ∀ i t x, HasDerivAt (fun s => B (φ i s x)) (dB i (φ i t x)) t)
       (hZ : ∀ i t x, HasDerivAt (fun s => Z i (φ i s x)) (dZ i (φ i t x)) t) :
       (∫ x, m x * inner ℝ (B x) (∑ i, dZ i x) +
         ∑ i, dm i x * inner ℝ (B x) (Z i x) ∂μ) =
         -(∫ x, m x * (∑ i, inner ℝ (dB i x) (Z i x)) ∂μ) := by
   …

2. theorem OAI.PositiveEinsteinFour.Averages.hasDerivAt_trace_block line 62

   Source documentation

   Ordinary differentiation of the trace curvature coefficient.

   theorem hasDerivAt_trace_block {v : ℝ → ℝ} {T N : ℝ → E}
       {dv : ℝ} {dT dN : E} {t : ℝ}
       (hv : HasDerivAt v dv t) (hT : HasDerivAt T dT t) (hN : HasDerivAt N dN t) :
       HasDerivAt (fun s => (4 + v s ^ 2) • T s - (5 : ℝ) • N s)
         ((4 + v t ^ 2) • dT + (2 * v t * dv) • T t - (5 : ℝ) • dN) t := by
   …

3. theorem OAI.PositiveEinsteinFour.Averages.trace_derivative_pairing line 74

   Source documentation

   The derivative of (4+v²)T-5N, after dN=2B_F(T)dT, gives exactly the normalized trace contribution used in equation (11).

   theorem trace_derivative_pairing
       (T : E) (Z AZ : Fin 4 → E) (v e B : ℝ) (p : Fin 4 → ℝ)
       (he : (∑ i, ‖Z i‖ ^ 2) = 6 * e)
       (hB : (∑ i, inner ℝ (AZ i) (Z i)) = 6 * B)
       (hp : ∀ i, inner ℝ T (Z i) = 6 * v * p i) :
       (5 / 12 : ℝ) * (∑ i, inner ℝ
         ((4 + v ^ 2) • Z i + (2 * v * p i) • T - (10 : ℝ) • AZ i) (Z i)) =
           (10 + (5 / 2) * v ^ 2) * e - 25 * B + 5 * v ^ 2 * (∑ i, p i ^ 2) := by
   …

4. theorem OAI.PositiveEinsteinFour.Averages.weighted_trace_contribution line 96

   Source documentation

   Both prescribed-trace subtractions integrate to the displayed first-derivative contribution. All hypotheses are raw flow derivatives and pointwise tensor contractions.

   theorem weighted_trace_contribution
       (φ : Fin 4 → ℝ → Ω ≃ᵐ Ω)
       (hφ : ∀ i, Continuous (fun p : ℝ × Ω => φ i p.1 p.2))
       (hμ : ∀ i t, MeasurePreserving (φ i t) μ μ)
       (m : C(Ω, ℝ)) (dm : Fin 4 → C(Ω, ℝ))
       (B0 : C(Ω, E)) (dB0 Z dZ : Fin 4 → C(Ω, E))
       (T : Ω → E) (AZ : Fin 4 → Ω → E)
       (v e B : Ω → ℝ) (p : Fin 4 → Ω → ℝ)
       (hm : ∀ i t x, HasDerivAt (fun s => m (φ i s x)) (dm i (φ i t x)) t)
       (hB0 : ∀ i t x, HasDerivAt (fun s => B0 (φ i s x)) (dB0 i (φ i t x)) t)
       (hZ : ∀ i t x, HasDerivAt (fun s => Z i (φ i s x)) (dZ i (φ i t x)) t)
       (hdB0 : ∀ i x, dB0 i x = (4 + v x ^ 2) • Z i x +
   …