def
definition
c2DischargeCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.Calculus.RadialDerivativesProofs on GitHub at line 482.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
C2DischargeCert -
differentiableAt_coordRay_partialDeriv_v2_radialInv_proved -
laplacian_radialInv_zero_no_const_proved -
partialDeriv_v2_radialInv_proved -
partialDeriv_v2_spatialRadius_proved -
spatialRadius_coordRay_ne_zero_proved
used by
formal source
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