IndisputableMonolith.Relativity.Calculus.Derivatives

declarations in this module (51)

• def basisVec L12
• lemma basisVec_self L14
• lemma basisVec_ne L16
• def coordRay L20
• lemma coordRay_apply L23
• lemma coordRay_zero L26
• lemma coordRay_coordRay L29
• def partialDeriv_v2 L34
• lemma partialDeriv_v2_const L39
• def secondDeriv L49
• def laplacian L54
• lemma deriv_add_lin L60
• lemma partialDeriv_v2_smul L69
• lemma secondDeriv_smul_local L77
• lemma secondDeriv_smul L92
• lemma laplacian_smul L105
• lemma partialDeriv_v2_mul L114
• def spatialNormSq L129
• theorem spatialNormSq_nonneg L131
• theorem spatialNormSq_eq_zero_iff L135
• def spatialRadius L151
• theorem spatialRadius_pos_iff L153
• theorem spatialRadius_ne_zero_iff L157
• theorem spatialRadius_pos_of_ne_zero L162
• lemma coordRay_temporal_spatial L168
• lemma spatialNormSq_coordRay_temporal L173
• lemma spatialRadius_coordRay_temporal L182
• lemma sq_le_spatialNormSq_1 L188
• lemma sq_le_spatialNormSq_2 L192
• lemma sq_le_spatialNormSq_3 L196
• lemma spatialNormSq_coordRay_spatial_1 L202
• lemma spatialNormSq_coordRay_spatial_2 L210
• lemma spatialNormSq_coordRay_spatial_3 L218
• theorem spatialRadius_coordRay_ne_zero L239
• def radialInv L346
• theorem differentiableAt_coordRay_i L350
• theorem differentiableAt_coordRay_i_sq L360
• theorem partialDeriv_v2_x_sq L365
• theorem deriv_coordRay_i L383
• theorem deriv_coordRay_j L388
• theorem partialDeriv_v2_spatialNormSq L398
• theorem differentiableAt_coordRay_spatialNormSq L409
• theorem differentiableAt_coordRay_spatialRadius L419
• theorem differentiableAt_coordRay_radialInv L428
• theorem spatialRadius_coordRay_ne_zero_eventually L442
• theorem partialDeriv_v2_spatialRadius L459
• theorem partialDeriv_v2_radialInv L509
• theorem differentiableAt_coordRay_partialDeriv_v2_radialInv L596
• theorem secondDeriv_radialInv L646
• theorem laplacian_radialInv_zero_no_const L769
• theorem laplacian_radialInv_n L808