· Kristi.AsymmetricGraph Kristi/Algorithms/ATSP.lean:17 abbrev
? Kristi.atsp_inapprox Kristi/Algorithms/ATSP.lean:20 theorem
? Kristi.atsp_inapprox_higher Kristi/Algorithms/ATSP.lean:24 theorem
? Kristi.atsp_gap_wider Kristi/Algorithms/ATSP.lean:34 theorem
? Kristi.atsp_inapprox_decimal Kristi/Algorithms/ATSP.lean:40 theorem
? Kristi.inapprox_comparison Kristi/Algorithms/ATSP.lean:44 theorem
· Kristi.EuclideanTSPInstance Kristi/Algorithms/AroraPTAS.lean:41 structure
· Kristi.aroraEuclidDist Kristi/Algorithms/AroraPTAS.lean:46 def
? Kristi.aroraEuclidDist_nonneg Kristi/Algorithms/AroraPTAS.lean:50 theorem
? Kristi.aroraEuclidDist_symm Kristi/Algorithms/AroraPTAS.lean:55 theorem
? Kristi.aroraEuclidDist_triangle Kristi/Algorithms/AroraPTAS.lean:62 theorem
· Kristi.euclidToMetric Kristi/Algorithms/AroraPTAS.lean:90 def
· Kristi.QuadtreeCell Kristi/Algorithms/AroraPTAS.lean:101 structure
· Kristi.portalsPerSide Kristi/Algorithms/AroraPTAS.lean:114 def
? Kristi.portals_increase Kristi/Algorithms/AroraPTAS.lean:118 theorem
? Kristi.arora_ptas_existence Kristi/Algorithms/AroraPTAS.lean:141 theorem
? Kristi.ptas_runtime_exponent Kristi/Algorithms/AroraPTAS.lean:147 theorem
? Kristi.rao_smith_improvement Kristi/Algorithms/AroraPTAS.lean:157 theorem
? Kristi.ptas_beats_christofides Kristi/Algorithms/AroraPTAS.lean:166 theorem
? Kristi.ptas_euclidean_only Kristi/Algorithms/AroraPTAS.lean:172 theorem
? Kristi.practical_crossover Kristi/Algorithms/AroraPTAS.lean:177 theorem
? Kristi.ptas_dimension_explosion Kristi/Algorithms/AroraPTAS.lean:182 theorem
? Kristi.euclidean_vs_metric Kristi/Algorithms/AroraPTAS.lean:190 theorem
· Kristi.degreeTwoLowerBound Kristi/Algorithms/Bounds.lean:15 def
? Kristi.degree_two_valid Kristi/Algorithms/Bounds.lean:21 theorem
? Kristi.bound_hierarchy_conditional Kristi/Algorithms/Bounds.lean:27 theorem
? Kristi.tour_edge_count Kristi/Algorithms/Bounds.lean:32 theorem
? Kristi.every_city_visited Kristi/Algorithms/Bounds.lean:36 theorem
? Kristi.min_edge_lower_bound Kristi/Algorithms/Bounds.lean:40 theorem
? Kristi.integrality_gap_conjecture_strict Kristi/Algorithms/Bounds.lean:48 theorem
· Kristi.SpanningTree Kristi/Algorithms/Christofides.lean:8 structure
· Kristi.spanningTreeWeight Kristi/Algorithms/Christofides.lean:13 def
? Kristi.spanningTreeWeight_nonneg Kristi/Algorithms/Christofides.lean:17 theorem
· Kristi.mstWeight Kristi/Algorithms/Christofides.lean:22 def
? Kristi.mst_le_any Kristi/Algorithms/Christofides.lean:27 theorem
? Kristi.mst_lower_bound Kristi/Algorithms/Christofides.lean:34 theorem
? Kristi.christofides_algebra Kristi/Algorithms/Christofides.lean:42 theorem
? Kristi.christofides_full Kristi/Algorithms/Christofides.lean:47 theorem
· Kristi.Comparison.christofides_ratio Kristi/Algorithms/Comparison.lean:12 def
· Kristi.Comparison.double_tree_ratio Kristi/Algorithms/Comparison.lean:13 def
· Kristi.Comparison.metric_inapprox Kristi/Algorithms/Comparison.lean:14 def
· Kristi.Comparison.atsp_inapprox Kristi/Algorithms/Comparison.lean:15 def
· Kristi.Comparison.four_thirds Kristi/Algorithms/Comparison.lean:16 def
· Kristi.Comparison.quantum_base Kristi/Algorithms/Comparison.lean:17 def
? Kristi.Comparison.chain_1_lt_atsp Kristi/Algorithms/Comparison.lean:21 theorem
? Kristi.Comparison.chain_metric_lt_atsp Kristi/Algorithms/Comparison.lean:22 theorem
? Kristi.Comparison.chain_metric_lt_4_3 Kristi/Algorithms/Comparison.lean:23 theorem
? Kristi.Comparison.chain_4_3_lt_christofides Kristi/Algorithms/Comparison.lean:24 theorem
? Kristi.Comparison.chain_christofides_lt_quantum Kristi/Algorithms/Comparison.lean:25 theorem
? Kristi.Comparison.chain_quantum_lt_dt Kristi/Algorithms/Comparison.lean:26 theorem
? Kristi.Comparison.full_chain Kristi/Algorithms/Comparison.lean:29 theorem
? Kristi.Comparison.gap_1_to_atsp Kristi/Algorithms/Comparison.lean:36 theorem
? Kristi.Comparison.gap_metric_to_atsp Kristi/Algorithms/Comparison.lean:37 theorem
? Kristi.Comparison.gap_metric_to_4_3 Kristi/Algorithms/Comparison.lean:38 theorem
? Kristi.Comparison.gap_4_3_to_christofides Kristi/Algorithms/Comparison.lean:39 theorem
? Kristi.Comparison.gap_christofides_to_dt Kristi/Algorithms/Comparison.lean:40 theorem
? Kristi.Comparison.christofides_over_dt Kristi/Algorithms/Comparison.lean:44 theorem
? Kristi.Comparison.ptas_beats_christofides Kristi/Algorithms/Comparison.lean:50 theorem
? Kristi.Comparison.ptas_runtime_explosion Kristi/Algorithms/Comparison.lean:53 theorem
? Kristi.Comparison.quantum_speedup_in_base Kristi/Algorithms/Comparison.lean:57 theorem
? Kristi.Comparison.quantum_speedup_in_base_upper Kristi/Algorithms/Comparison.lean:58 theorem
? Kristi.Comparison.held_karp_speedup_10 Kristi/Algorithms/Comparison.lean:62 theorem
? Kristi.Comparison.held_karp_speedup_15 Kristi/Algorithms/Comparison.lean:63 theorem
? Kristi.Comparison.held_karp_speedup_20 Kristi/Algorithms/Comparison.lean:64 theorem
? Kristi.Comparison.atsp_upper_unbounded Kristi/Algorithms/Comparison.lean:68 theorem
? Kristi.Comparison.symmetric_much_tighter Kristi/Algorithms/Comparison.lean:69 theorem
? Kristi.Comparison.total_improvement_christofides_over_brute Kristi/Algorithms/Comparison.lean:73 theorem
? Kristi.Comparison.inapprox_gap_metric Kristi/Algorithms/Comparison.lean:79 theorem
? Kristi.Comparison.inapprox_gap_atsp Kristi/Algorithms/Comparison.lean:82 theorem
? Kristi.lp_root_gap_small Kristi/Algorithms/Concorde.lean:27 theorem
? Kristi.concorde_empirical_scaling Kristi/Algorithms/Concorde.lean:31 theorem
? Kristi.lp_much_tighter_than_mst Kristi/Algorithms/Concorde.lean:36 theorem
? Kristi.lkh_practical_quality Kristi/Algorithms/Concorde.lean:44 theorem
? Kristi.subtour_count_exponential Kristi/Algorithms/Concorde.lean:49 theorem
? Kristi.subtour_constraints_count_5 Kristi/Algorithms/Concorde.lean:56 theorem
? Kristi.subtour_constraints_count_10 Kristi/Algorithms/Concorde.lean:57 theorem
? Kristi.double_tree_approximation Kristi/Algorithms/DoubleTree.lean:8 theorem
? Kristi.christofides_beats_double_tree Kristi/Algorithms/DoubleTree.lean:13 theorem
? Kristi.improvement_ratio Kristi/Algorithms/DoubleTree.lean:16 theorem
? Kristi.matching_saves_over_doubling Kristi/Algorithms/DoubleTree.lean:19 theorem
? Kristi.sebo_vygen_better Kristi/Algorithms/GraphicTSP.lean:25 theorem
? Kristi.sebo_vygen_improvement Kristi/Algorithms/GraphicTSP.lean:28 theorem
? Kristi.sebo_vygen_pct Kristi/Algorithms/GraphicTSP.lean:31 theorem
? Kristi.momke_svensson Kristi/Algorithms/GraphicTSP.lean:34 theorem
? Kristi.mucha_ratio Kristi/Algorithms/GraphicTSP.lean:37 theorem
? Kristi.graphic_tsp_chain Kristi/Algorithms/GraphicTSP.lean:40 theorem
? Kristi.kko_epsilon Kristi/Algorithms/GraphicTSP.lean:46 theorem
? Kristi.sebo_vygen_vs_kko Kristi/Algorithms/GraphicTSP.lean:49 theorem
? Kristi.graphic_hierarchy Kristi/Algorithms/GraphicTSP.lean:52 theorem
? Kristi.graphic_easier Kristi/Algorithms/GraphicTSP.lean:57 theorem
· Kristi.greedyTour Kristi/Algorithms/Greedy.lean:19 def
? Kristi.greedy_time_cubic Kristi/Algorithms/Greedy.lean:27 theorem
· Kristi.heldKarpDP Kristi/Algorithms/HeldKarp.lean:15 def
· Kristi.heldKarpOpt Kristi/Algorithms/HeldKarp.lean:23 def
? Kristi.heldKarpDP_base Kristi/Algorithms/HeldKarp.lean:29 theorem
? Kristi.exp_le_factorial Kristi/Algorithms/HeldKarp.lean:34 theorem
? Kristi.held_karp_states_le Kristi/Algorithms/HeldKarp.lean:46 theorem
? Kristi.held_karp_dp_count Kristi/Algorithms/HeldKarp.lean:56 theorem
· Kristi.KOptNeighbor Kristi/Algorithms/KOpt.lean:40 def
· Kristi.IsKOptLocalOpt Kristi/Algorithms/KOpt.lean:44 def
+2,270 more — narrow with filters