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

cross_term_factored

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)

  54theorem cross_term_factored (ε₁ ε₂ : ℝ)
  55    (h1 : -(1 : ℝ) < ε₁) (h2 : -(1 : ℝ) < ε₂) (h12 : -(1 : ℝ) < ε₁ + ε₂) :
  56    superposition_cross_term ε₁ ε₂ =
  57      (ε₁ + ε₂) ^ 2 / (2 * (1 + (ε₁ + ε₂))) -
  58      ε₁ ^ 2 / (2 * (1 + ε₁)) -
  59      ε₂ ^ 2 / (2 * (1 + ε₂)) := by

proof body

Term-mode proof.

  60  unfold superposition_cross_term
  61  rw [Jcost_one_plus_exact _ h12, Jcost_one_plus_exact _ h1, Jcost_one_plus_exact _ h2]
  62
  63/-! ## 2. Weak-Field Superposition for Processing Fields -/
  64
  65/-- Two independent processing fields (gravitational + external).
  66    In the weak-field regime, their combined effect is their sum. -/

depends on (9)

Lean names referenced from this declaration's body.