FlowGreen.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts from invariance of the frame-flow measure. The only derivative hypotheses concern individual continuous fields along the flow; the weighted identity is derived using the product rule.

def OAI.PositiveEinsteinFour.Averages.fieldIntegral line 25
theorem OAI.PositiveEinsteinFour.Averages.fieldIntegral_apply line 28

theorem OAI.PositiveEinsteinFour.Averages.integral_flow_derivative_zero line 37

Source documentation

The integral of a continuous infinitesimal generator is zero. This is obtained by differentiating the invariant integral, not assumed as a separate integration-by-parts law.

theorem integral_flow_derivative_zero
    (φ : ℝ → Ω ≃ᵐ Ω)
    (hφ : Continuous (fun p : ℝ × Ω => φ p.1 p.2))
    (hμ : ∀ t, MeasurePreserving (φ t) μ μ)
    (f d : C(Ω, ℝ))
    (hd : ∀ t x, HasDerivAt (fun s => f (φ s x)) (d (φ t x)) t) :
    (∫ x, d x ∂μ) = 0 := by
…

theorem OAI.PositiveEinsteinFour.Averages.weighted_flow_green line 68

Source documentation

Weighted Green identity for any two tensor-coordinate fields along a measure-preserving parallel-frame flow.

theorem weighted_flow_green
    (φ : ℝ → Ω ≃ᵐ Ω)
    (hφ : Continuous (fun p : ℝ × Ω => φ p.1 p.2))
    (hμ : ∀ t, MeasurePreserving (φ t) μ μ)
    (m dm : C(Ω, ℝ)) (f df g dg : C(Ω, E))
    (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)
    (hg : ∀ t x, HasDerivAt (fun s => g (φ s x)) (dg (φ t x)) t) :
    (∫ x, m x * inner ℝ (df x) (g x) +
      dm x * inner ℝ (f x) (g x) ∂μ) =
      -(∫ x, m x * inner ℝ (f x) (dg x) ∂μ) := by
…

theorem OAI.PositiveEinsteinFour.Averages.weighted_four_direction_green line 103

Source documentation

Sum the four parallel-frame directions. This is the weighted rough Laplacian identity used for the covariant Weyl gradient.

theorem weighted_four_direction_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))
    (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) :
    (∫ x, m x * (∑ i, ‖df i x‖ ^ 2) +
      ∑ i, dm i x * inner ℝ (f x) (df i x) ∂μ) =
      -(∫ x, m x * inner ℝ (f x) (∑ i, ddf i x) ∂μ) := by
…