· Audrey.Collision.V2 Audrey/Collision/Momentum.lean:47 abbrev
· Audrey.Collision.BinaryCollision Audrey/Collision/Momentum.lean:53 structure
· Audrey.Collision.sqNorm Audrey/Collision/Momentum.lean:60 def
? Audrey.Collision.sqNorm_nonneg Audrey/Collision/Momentum.lean:62 theorem
? Audrey.Collision.sqNorm_zero_of_zero Audrey/Collision/Momentum.lean:68 theorem
· Audrey.Collision.totalMomentum Audrey/Collision/Momentum.lean:74 def
· Audrey.Collision.totalKineticEnergy Audrey/Collision/Momentum.lean:77 def
· Audrey.Collision.ConservesMomentum Audrey/Collision/Momentum.lean:82 def
· Audrey.Collision.ConservesEnergy Audrey/Collision/Momentum.lean:87 def
· Audrey.Collision.IsElastic Audrey/Collision/Momentum.lean:92 def
· Audrey.Collision.IsHitAndStickSetup Audrey/Collision/Momentum.lean:98 def
· Audrey.Collision.HitAndStickOutcome Audrey/Collision/Momentum.lean:103 def
? Audrey.Collision.hit_and_stick_kinematics Audrey/Collision/Momentum.lean:108 theorem
? Audrey.Collision.hit_and_stick_energy_transfer Audrey/Collision/Momentum.lean:124 theorem
· Audrey.Collision.IsPeelSetup Audrey/Collision/Momentum.lean:131 def
? Audrey.Collision.peel_invariance Audrey/Collision/Momentum.lean:143 theorem
· Audrey.Collision.DoubleTakeoutAdmissible Audrey/Collision/Momentum.lean:159 def
? Audrey.Collision.double_takeout_geometry Audrey/Collision/Momentum.lean:171 theorem
· Audrey.Collision.IsRaiseSetup Audrey/Collision/Momentum.lean:185 def
? Audrey.Collision.raise_energy_floor Audrey/Collision/Momentum.lean:191 theorem
? Audrey.Collision.elastic_energy_identity Audrey/Collision/Momentum.lean:199 theorem
? Audrey.Collision.elastic_momentum_identity Audrey/Collision/Momentum.lean:206 theorem
· Audrey.Collision.CollisionKind Audrey/Collision/Momentum.lean:213 inductive
· Audrey.Constants.g Audrey/Constants.lean:50 def
? Audrey.Constants.g_pos Audrey/Constants.lean:52 theorem
· Audrey.Constants.pi Audrey/Constants.lean:56 def
· Audrey.Constants.stoneMassMax Audrey/Constants.lean:63 def
· Audrey.Constants.stoneMassMin Audrey/Constants.lean:67 def
· Audrey.Constants.stoneMass Audrey/Constants.lean:71 def
· Audrey.Constants.stoneCircumferenceMax Audrey/Constants.lean:75 def
· Audrey.Constants.stoneRadiusMax Audrey/Constants.lean:79 def
· Audrey.Constants.stoneHeightMin Audrey/Constants.lean:82 def
· Audrey.Constants.runningBandRadius Audrey/Constants.lean:88 def
· Audrey.Constants.stoneMoment Audrey/Constants.lean:94 def
? Audrey.Constants.stoneMass_pos Audrey/Constants.lean:96 theorem
? Audrey.Constants.stoneMass_le_max Audrey/Constants.lean:97 theorem
? Audrey.Constants.stoneMassMin_le_stoneMass Audrey/Constants.lean:98 theorem
? Audrey.Constants.runningBandRadius_pos Audrey/Constants.lean:100 theorem
· Audrey.Constants.sheetLength Audrey/Constants.lean:106 def
· Audrey.Constants.sheetWidth Audrey/Constants.lean:109 def
· Audrey.Constants.nearHog Audrey/Constants.lean:113 def
· Audrey.Constants.farHog Audrey/Constants.lean:117 def
· Audrey.Constants.teeLine Audrey/Constants.lean:121 def
· Audrey.Constants.backLine Audrey/Constants.lean:125 def
· Audrey.Constants.houseRadius Audrey/Constants.lean:128 def
· Audrey.Constants.eightFootRadius Audrey/Constants.lean:131 def
· Audrey.Constants.fourFootRadius Audrey/Constants.lean:134 def
· Audrey.Constants.buttonRadius Audrey/Constants.lean:137 def
? Audrey.Constants.nearHog_lt_farHog Audrey/Constants.lean:139 theorem
? Audrey.Constants.farHog_lt_teeLine Audrey/Constants.lean:140 theorem
? Audrey.Constants.teeLine_lt_backLine Audrey/Constants.lean:141 theorem
? Audrey.Constants.buttonRadius_lt_houseRadius Audrey/Constants.lean:142 theorem
· Audrey.Constants.muIceCold Audrey/Constants.lean:150 def
· Audrey.Constants.muIceSwept Audrey/Constants.lean:155 def
· Audrey.Constants.muIce Audrey/Constants.lean:158 def
? Audrey.Constants.muIce_pos Audrey/Constants.lean:160 theorem
? Audrey.Constants.muIceSwept_lt_muIce Audrey/Constants.lean:161 theorem
· Audrey.Constants.sweepFrictionRatio Audrey/Constants.lean:165 def
· Audrey.Constants.standardDrawVelocity Audrey/Constants.lean:174 def
· Audrey.Constants.standardSpin Audrey/Constants.lean:185 def
· Audrey.Constants.standardDeliveryTime Audrey/Constants.lean:190 def
· Audrey.Constants.measuredCurlDistance Audrey/Constants.lean:196 def
? Audrey.Constants.standardSpin_pos Audrey/Constants.lean:198 theorem
· Audrey.Constants.hammerValue Audrey/Constants.lean:206 def
? Audrey.Constants.hammerValue_first_end_kws2001 Audrey/Constants.lean:221 theorem
? Audrey.Constants.hammerValue_last_end_kws2001 Audrey/Constants.lean:224 theorem
? Audrey.Constants.hammerValue_monotone_within_game Audrey/Constants.lean:228 theorem
· Audrey.Constants.pebbleDensity Audrey/Constants.lean:252 def
· Audrey.Constants.pebbleHeight Audrey/Constants.lean:256 def
· Audrey.Constants.pebbleRadius Audrey/Constants.lean:259 def
? Audrey.Constants.pebbleDensity_pos Audrey/Constants.lean:261 theorem
· Audrey.FirstPrinciples.AsymmetricFriction.staticBandPressure Audrey/FirstPrinciples/AsymmetricFriction.lean:82 def
? Audrey.FirstPrinciples.AsymmetricFriction.staticBandPressure_pos Audrey/FirstPrinciples/AsymmetricFriction.lean:84 theorem
· Audrey.FirstPrinciples.AsymmetricFriction.frontLoadFactor Audrey/FirstPrinciples/AsymmetricFriction.lean:99 def
· Audrey.FirstPrinciples.AsymmetricFriction.backLoadFactor Audrey/FirstPrinciples/AsymmetricFriction.lean:102 def
? Audrey.FirstPrinciples.AsymmetricFriction.load_factors_sum_to_two Audrey/FirstPrinciples/AsymmetricFriction.lean:105 theorem
? Audrey.FirstPrinciples.AsymmetricFriction.frontLoadFactor_gt_one Audrey/FirstPrinciples/AsymmetricFriction.lean:113 theorem
· Audrey.FirstPrinciples.AsymmetricFriction.localFrictionCoefficient Audrey/FirstPrinciples/AsymmetricFriction.lean:131 def
? Audrey.FirstPrinciples.AsymmetricFriction.localFrictionCoefficient_at_static Audrey/FirstPrinciples/AsymmetricFriction.lean:134 theorem
? Audrey.FirstPrinciples.AsymmetricFriction.localFriction_decreases_with_pressure Audrey/FirstPrinciples/AsymmetricFriction.lean:143 theorem
· Audrey.FirstPrinciples.AsymmetricFriction.curlForceConstant Audrey/FirstPrinciples/AsymmetricFriction.lean:164 def
· Audrey.FirstPrinciples.AsymmetricFriction.lateralCurlForce Audrey/FirstPrinciples/AsymmetricFriction.lean:167 def
? Audrey.FirstPrinciples.AsymmetricFriction.lateralCurlForce_linear_in_omega Audrey/FirstPrinciples/AsymmetricFriction.lean:170 theorem
? Audrey.FirstPrinciples.AsymmetricFriction.lateralCurlForce_inverse_in_v Audrey/FirstPrinciples/AsymmetricFriction.lean:179 theorem
? Audrey.FirstPrinciples.AsymmetricFriction.asymmetric_pressure_implies_lateral_force Audrey/FirstPrinciples/AsymmetricFriction.lean:193 theorem
· Audrey.FirstPrinciples.AsymmetricFriction.standardCurlForceConstant Audrey/FirstPrinciples/AsymmetricFriction.lean:213 def
? Audrey.FirstPrinciples.AsymmetricFriction.standardCurlForceConstant_pos Audrey/FirstPrinciples/AsymmetricFriction.lean:216 theorem
· Audrey.FirstPrinciples.EnergyConservation.velocityAt Audrey/FirstPrinciples/EnergyConservation.lean:49 def
· Audrey.FirstPrinciples.EnergyConservation.positionAt Audrey/FirstPrinciples/EnergyConservation.lean:52 def
· Audrey.FirstPrinciples.EnergyConservation.stoppingTime Audrey/FirstPrinciples/EnergyConservation.lean:55 def
· Audrey.FirstPrinciples.EnergyConservation.stoppingDistance Audrey/FirstPrinciples/EnergyConservation.lean:58 def
? Audrey.FirstPrinciples.EnergyConservation.velocity_zero_at_stoppingTime Audrey/FirstPrinciples/EnergyConservation.lean:63 theorem
? Audrey.FirstPrinciples.EnergyConservation.position_at_stoppingTime_eq_stoppingDistance Audrey/FirstPrinciples/EnergyConservation.lean:73 theorem
? Audrey.FirstPrinciples.EnergyConservation.drawVelocity_sq Audrey/FirstPrinciples/EnergyConservation.lean:89 theorem
? Audrey.FirstPrinciples.EnergyConservation.drawVelocity_from_stoppingDistance Audrey/FirstPrinciples/EnergyConservation.lean:99 theorem
? Audrey.FirstPrinciples.EnergyConservation.standardDrawVelocity_from_energy Audrey/FirstPrinciples/EnergyConservation.lean:121 theorem
? Audrey.FirstPrinciples.EnergyConservation.standardDrawVelocity_pos Audrey/FirstPrinciples/EnergyConservation.lean:126 theorem
? Audrey.FirstPrinciples.EnergyConservation.standardDrawVelocity_sq_eq Audrey/FirstPrinciples/EnergyConservation.lean:138 theorem
· Audrey.FirstPrinciples.HammerFromBackwardInduction.EndOutcomeDistribution Audrey/FirstPrinciples/HammerFromBackwardInduction.lean:81 structure
· Audrey.FirstPrinciples.HammerFromBackwardInduction.expectedSingleEndSwing Audrey/FirstPrinciples/HammerFromBackwardInduction.lean:104 def
+984 more — narrow with filters