OAI/Combinatorics/ThinTrees/Metric/Response.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Metric response.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.laplacian_mono line 18
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.restrict_laplacian line 26
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.restrict_laplacian_le line 32
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.metric_shortcut_response line 37
  5. theorem OAI.AlgorithmicThinTrees.MetricTests.simultaneous_metric_response_bound line 93
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.quarter_negative_power line 127
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.response_fraction_cutoff line 140
  8. theorem OAI.AlgorithmicThinTrees.MetricTests.simultaneous_metric_response line 185