is

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

• optimalT60 in IndisputableMonolith.Acoustics.RoomAcousticsSabineFromJCost decl_use
• hearingLossPenalty in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
• hearingLossPenalty_zero in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
• applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
• energyConservationCert in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
• christoffel in IndisputableMonolith.Action.EulerLagrange decl_use
• const_one_is_geodesic in IndisputableMonolith.Action.EulerLagrange decl_use
• costRateEL_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
• costRateEL_iff_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
• costRateEL_implies_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
• geodesicEquationHolds in IndisputableMonolith.Action.EulerLagrange decl_use
• geodesic_iff_hessianEnergy_EL in IndisputableMonolith.Action.EulerLagrange decl_use
• actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
• actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
• actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use
• geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
• Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
• energy_conservation in IndisputableMonolith.Action.Hamiltonian decl_use
• hamiltonPDotEquation in IndisputableMonolith.Action.Hamiltonian decl_use
• totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
• newtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
• NewtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
• spaceShift in IndisputableMonolith.Action.Noether decl_use
• spaceTranslationFlow in IndisputableMonolith.Action.Noether decl_use
• space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
• timeShift in IndisputableMonolith.Action.Noether decl_use
• timeTranslationFlow in IndisputableMonolith.Action.Noether decl_use
• actionJ_def in IndisputableMonolith.Action.PathSpace decl_use
• const_apply in IndisputableMonolith.Action.PathSpace decl_use
• fixedEndpoints_trans in IndisputableMonolith.Action.PathSpace decl_use

… and 10 more