integrate_add

formal source

  51
  52/-- Integration is linear (finite weighted sum).
  53    STATUS: PROVED — Linearity of finite sums. -/
  54theorem integrate_add (f₁ f₂ : (Fin 4 → ℝ) → ℝ) (g : MetricTensor) (vol : VolumeElement) :
  55    integrate_scalar (fun x => f₁ x + f₂ x) g vol =
  56      integrate_scalar f₁ g vol + integrate_scalar f₂ g vol := by
  57  unfold integrate_scalar
  58  simp [Finset.sum_add_distrib, mul_add]
  59
  60/-- Integration scaling property.
  61    STATUS: PROVED — Scaling of finite sums. -/
  62theorem integrate_smul (c : ℝ) (f : (Fin 4 → ℝ) → ℝ) (g : MetricTensor) (vol : VolumeElement) :
  63    integrate_scalar (fun x => c * f x) g vol =
  64      c * integrate_scalar f g vol := by
  65  unfold integrate_scalar
  66  -- LHS: Δx4 * Σᵢ (sqrt_g * (c * f)) = Δx4 * Σᵢ (c * sqrt_g * f)
  67  -- RHS: c * (Δx4 * Σᵢ sqrt_g * f)
  68  have h : ∀ i : ℕ, sqrt_minus_g g (fun _ => (i : ℝ) * vol.grid_spacing) *
  69      (c * f (fun _ => (i : ℝ) * vol.grid_spacing)) =
  70    c * (sqrt_minus_g g (fun _ => (i : ℝ) * vol.grid_spacing) *
  71      f (fun _ => (i : ℝ) * vol.grid_spacing)) := by intro i; ring
  72  simp_rw [h]
  73  rw [← Finset.mul_sum]
  74  ring
  75
  76/-- Kinetic action is nonnegative for positive-signature spatial parts.
  77    STATUS: SCAFFOLD — Proof simplified with placeholder sqrt_minus_g = 1. -/
  78theorem kinetic_nonneg (φ : ScalarField) (g : MetricTensor) (vol : VolumeElement)
  79    (hSign : ∀ x, 0 ≤ gradient_squared φ g x) :
  80  0 ≤ kinetic_action φ g vol := by
  81  unfold kinetic_action integrate_scalar sqrt_minus_g
  82  apply mul_nonneg (by norm_num)
  83  apply mul_nonneg (pow_nonneg (le_of_lt vol.grid_spacing_pos) 4)
  84  apply Finset.sum_nonneg