IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance

declarations in this module (597)

• def CanonicalHessianIsDirichlet L39
• theorem canonicalHessianIsDirichlet_of_encodedPeriodicFreudenthal L46
• abbrev PhysicalFiniteDifferenceDirichletAction L55
• def PhysicalFiniteDifferenceDirichletTarget L63
• def periodicEdgeStencilDirichletAction L73
• def periodicAxisDisp L81
• def canonicalPeriodicMixedAxisStencilAction L88
• def PeriodicEdgeStencilDirichletTarget L100
• theorem periodicEdgeStencilDirichletAction_nonneg L106
• theorem periodicEdgeStencilTarget_of_noSelfLoop L113
• theorem canonicalPeriodicNoSelfLoopEdges L122
• theorem canonicalPeriodicEdgeStencilTarget L134
• theorem canonicalPeriodicJQuadraticTerm_eq_edgeStencil L143
• def CanonicalPeriodicEdgeStencilLocalCorrespondence L159
• def CanonicalPeriodicStrongestTrueReplacement L173
• theorem canonicalPeriodicStrongestTrueReplacement_iff_edgeStencilLocalCorrespondence L178
• theorem canonicalPeriodicEdgeStencilLocalCorrespondence_of_taylor L185
• theorem canonicalPeriodicEdgeStencilLocalCorrespondence_of_flat_and_remainderJets L206
• theorem supplies L232
• theorem canonicalPeriodicEdgeStencilLocalCorrespondence_of_flat_first_and_directionalHessian L234
• theorem canonicalPeriodicEdgeStencilLocalCorrespondence_of_eventuallyZero_edgeStencil_and_taylor L259
• theorem canonicalPeriodicEdgeStencilLocalCorrespondence_of_localHessianTaylorInputs L296
• theorem canonicalPeriodicStrongestTrueReplacement_of_localHessianTaylorInputs L320
• structure PeriodicFreudenthalDirichletCertificate L338
• def regularModel_of_periodicFreudenthalCertificate L356
• def physicalSixTetModel_of_periodicFreudenthalCertificate L368
• def cubicLimitInput_of_periodicFreudenthalCertificate L378
• theorem periodicFreudenthalCertificate_cubicLimit L386
• theorem periodicFreudenthalCertificate_error_vanishes_along_family L399
• theorem periodicFreudenthalCertificate_error_vanishes_of_bounded_error_and_spacing L424
• structure PeriodicFreudenthalRefinementFamily L455
• def exactPeriodicFreudenthalComparisonCertificate L527
• def exactPeriodicFreudenthalComparisonCertificateAtSpacing L548
• theorem exactPeriodicFreudenthalComparisonCertificateAtSpacing_converges L571
• def canonicalPeriodicEdgeStencilComparisonCertificate L598
• def canonicalPeriodicEdgeStencilComparisonCertificateAtSpacing L630
• def canonicalPeriodicEdgeStencilContinuumCertificateAtSpacing L664
• theorem canonicalPeriodicEdgeStencilComparisonCertificateAtSpacing_converges L702
• def canonicalPeriodicEdgeStencilRefinementFamily L733
• theorem canonicalPeriodicEdgeStencilRefinementFamily_pointwise_converges L751
• def canonicalPeriodicEdgeStencilContinuumRefinementFamily L776
• theorem canonicalPeriodicEdgeStencilContinuumRefinementFamily_pointwise_converges L811
• theorem canonicalPeriodicEdgeStencilContinuumRefinementFamily_converges_to_fixed_limit L851
• structure CanonicalPeriodicFixedContinuumComparisonData L900
• abbrev CanonicalPeriodicFixedPhysicalContinuumAction L1177
• structure CanonicalPeriodicFixedPhysicalActionComparisonData L1186
• def canonicalPeriodicFixedDirichletContinuumAction L1319
• theorem canonicalPeriodicFixedDirichletContinuumAction_eq_reggeSecondOrder L1336
• def canonicalPeriodicFixedDirichletActionComparisonData L1357
• theorem canonicalPeriodicFixedDirichletAction_pointwise_tendsto L1385
• theorem canonicalPeriodicFixedDirichletAction_weighted_finite_probe_residual_tendsto_zero L1409
• theorem canonicalPeriodicFixedDirichletAction_variable_weighted_finite_probe_residual_tendsto_zero L1442
• theorem canonicalPeriodicNonlinearResidual_bound_to_fixedDirichlet L1478
• theorem canonicalPeriodicNonlinearResidual_tendsto_zero_to_fixedDirichlet L1520
• theorem canonicalPeriodicNonlinearResidual_tendsto_zero_eventually_to_fixedDirichlet L1559
• theorem canonicalPeriodicNonlinearResidual_tendsto_zero_scaled_to_fixedDirichlet L1612
• theorem canonicalPeriodicNonlinearResidual_tendsto_zero_spacing_scaled_to_fixedDirichlet L1657
• theorem canonicalPeriodicNonlinearResidual_weighted_finite_probe_spacing_scaled_tendsto_zero L1686
• theorem canonicalPeriodicNonlinearResidual_variable_weighted_finite_probe_spacing_scaled_tendsto_zero L1748
• theorem canonicalPeriodicNonlinearResidual_variable_weighted_finite_probe_spacing_scaled_to_secondOrder_tendsto_zero L1813
• theorem canonicalPeriodicNonlinearAggregate_variable_weighted_finite_probe_spacing_scaled_to_secondOrder_residual_tendsto_zero L1856
• theorem canonicalPeriodicNonlinearResidual_variable_weighted_finite_probe_spacing_scaled_to_secondOrder_div_spacing_norm_sq_tendsto_zero L1901
• theorem canonicalPeriodicSecondOrder_variable_weighted_finite_probe_spacing_scaled_div_spacing_norm_sq_tendsto L2090
• def FlatDeficitZeroTarget L2152
• def FlatDeficitAngleSumTarget L2157
• theorem flatDeficitZeroTarget_of_angleSum L2164
• theorem flatDeficitZeroTarget_iff_globalZeroDeficitAtFlat L2184
• theorem globalZeroDeficitAtFlat_of_angleSum L2191
• def freudenthalLocalDihedralAngle L2200
• def canonicalPeriodicTypedEdgeAngleContribution L2206
• def CanonicalPeriodicTypedEdgeAngleSumTarget L2218
• def CanonicalPeriodicDirectTypedEdgeAngleSumTarget L2229
• def canonicalPeriodicTypedEdgeIncident L2238
• instance canonicalPeriodicTypedEdgeIncident_decidable L2244
• def canonicalPeriodicTypedEdgeIncidentSlotWitness L2255
• instance canonicalPeriodicTypedEdgeIncidentSlotWitness_decidable L2261
• theorem canonicalPeriodicTypedEdgeIncident_iff_slotWitness L2271
• theorem canonicalPeriodicTypedEdge_eq_localEdgeOf_of_slotWitness L2282
• theorem canonicalPeriodicTypedEdgeAngleContribution_eq_of_slot L2293
• def canonicalPeriodicTypedEdgeLocalEdgeOfWitness L2305

… and 517 more