pith. machine review for the scientific record. sign in
theorem proved tactic proof

integrate_smul

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Tactic-mode proof.

  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. -/

depends on (13)

Lean names referenced from this declaration's body.