C2DischargeCert

formal source

 465Net effect: Mathlib calculus axiom count in `Derivatives.lean` can drop from 13 to 6
 466once the `axiom` declarations are replaced with `theorem` + import of this file.
 467-/
 468structure C2DischargeCert where
 469  ne_zero_holds : ∀ (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
 470    (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2),
 471    spatialRadius (coordRay x ν s) ≠ 0
 472  partial_sr_holds : ∀ (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
 473    partialDeriv_v2 spatialRadius μ x = if μ = 0 then 0 else x μ / spatialRadius x
 474  partial_inv_holds : ∀ (n : ℕ) (μ : Fin 4) (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
 475    partialDeriv_v2 (radialInv n) μ x =
 476    if μ = 0 then 0 else -(n : ℝ) * x μ / (spatialRadius x) ^ (n + 2)
 477  diff_at_holds : ∀ (n : ℕ) (x : Fin 4 → ℝ) (μ ν : Fin 4) (hx : spatialRadius x ≠ 0),
 478    DifferentiableAt ℝ (fun s => partialDeriv_v2 (radialInv n) μ (coordRay x ν s)) 0
 479  lap_zero_holds : ∀ (x : Fin 4 → ℝ) (hx : spatialRadius x ≠ 0),
 480    laplacian (radialInv 1) x = 0
 481
 482def c2DischargeCert : C2DischargeCert where
 483  ne_zero_holds := spatialRadius_coordRay_ne_zero_proved
 484  partial_sr_holds := partialDeriv_v2_spatialRadius_proved
 485  partial_inv_holds := partialDeriv_v2_radialInv_proved
 486  diff_at_holds := differentiableAt_coordRay_partialDeriv_v2_radialInv_proved
 487  lap_zero_holds := laplacian_radialInv_zero_no_const_proved
 488
 489theorem c2DischargeCert_inhabited : Nonempty C2DischargeCert := ⟨c2DischargeCert⟩
 490
 491end Calculus
 492end Relativity
 493end IndisputableMonolith