integrate_smul

formal source

  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
  85  intro i _
  86  apply mul_nonneg (by norm_num : (0 : ℝ) ≤ 1)
  87  apply hSign
  88
  89
  90/-- Einstein-Hilbert action: (M_P^2/2) ∫ √(-g) R d^4x. -/
  91noncomputable def einstein_hilbert_action
  92  (g : MetricTensor) (M_P_squared : ℝ) (vol : VolumeElement) : ℝ :=