OAI/NumberTheory/Jacobsthal/Estimates/HarmonicConditioning.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseCells.harmonicMass line 15
  2. def OAI.Erdos970.ErdosInverseCells.tripleSpace line 17
  3. def OAI.Erdos970.ErdosInverseCells.tripleWeight line 19
  4. def OAI.Erdos970.ErdosInverseCells.weightedWitness line 22
  5. def OAI.Erdos970.ErdosInverseCells.cofactorReward line 25
  6. def OAI.Erdos970.ErdosInverseCells.conditionalReward line 28
  7. theorem OAI.Erdos970.ErdosInverseCells.harmonicMass_nonneg line 31
  8. theorem OAI.Erdos970.ErdosInverseCells.harmonicMass_pos line 33
  9. theorem OAI.Erdos970.ErdosInverseCells.tripleWeight_nonneg line 39
  10. theorem OAI.Erdos970.ErdosInverseCells.triple_weight_sum line 41
  11. theorem OAI.Erdos970.ErdosInverseCells.cofactorReward_nonneg line 45
  12. theorem OAI.Erdos970.ErdosInverseCells.cofactorReward_upper line 48
  13. theorem OAI.Erdos970.ErdosInverseCells.conditionalReward_bounds line 61
  14. theorem OAI.Erdos970.ErdosInverseCells.weightedWitness_decomposition line 66
  15. theorem OAI.Erdos970.ErdosInverseCells.weightedWitness_conditioning line 86
  16. theorem OAI.Erdos970.ErdosInverseCells.conditioned_reward_upper line 92
  17. theorem OAI.Erdos970.ErdosInverseCells.condition_harmonic_density line 99
  18. theorem OAI.Erdos970.ErdosInverseCells.uncondition_harmonic_density line 109