OAI/Analysis/C0Absorption/Frozen.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.C0Absorption.FrozenWeights line 14
  2. def OAI.C0Absorption.stateWeights line 21
  3. def OAI.C0Absorption.blockInput line 28
  4. def OAI.C0Absorption.rowScalar line 30
  5. theorem OAI.C0Absorption.rowScalar_apply line 33
  6. def OAI.C0Absorption.previousScalar line 37
  7. def OAI.C0Absorption.frozenCorrection line 42
  8. theorem OAI.C0Absorption.frozenCorrection_apply line 45
  9. def OAI.C0Absorption.correction line 48
  10. theorem OAI.C0Absorption.blockInput_abs_le line 50
  11. theorem OAI.C0Absorption.finiteRadius_mono line 55
  12. theorem OAI.C0Absorption.blockInput_le_radius line 63
  13. theorem OAI.C0Absorption.abs_finite_dot_le line 67
  14. theorem OAI.C0Absorption.rowScalar_bound line 78
  15. theorem OAI.C0Absorption.rowScalar_local line 83
  16. theorem OAI.C0Absorption.previousScalar_local line 87
  17. theorem OAI.C0Absorption.scalar_difference_bound line 103
  18. theorem OAI.C0Absorption.frozenCorrection_local line 107
  19. theorem OAI.C0Absorption.frozenCorrection_bound line 114
  20. theorem OAI.C0Absorption.frozenCorrection_distance line 118
  21. theorem OAI.C0Absorption.rowScalar_weight_error line 123
  22. structure OAI.C0Absorption.WeightError line 130
  23. theorem OAI.C0Absorption.previousScalar_weight_error line 134
  24. theorem OAI.C0Absorption.correction_weight_error line 142
  25. def OAI.C0Absorption.mixedState line 176
  26. def OAI.C0Absorption.mixedWeights line 179
  27. theorem OAI.C0Absorption.mixed_left_error line 186
  28. theorem OAI.C0Absorption.mixed_right_error line 203
  29. theorem OAI.C0Absorption.abs_sub_three line 220
  30. def OAI.C0Absorption.correctionL line 223
  31. theorem OAI.C0Absorption.correctionL_coe line 225
  32. theorem OAI.C0Absorption.correction_lipschitz line 227
  33. theorem OAI.C0Absorption.correction_local line 243
  34. theorem OAI.C0Absorption.correction_bound line 246
  35. theorem OAI.C0Absorption.correction_zero line 250
  36. theorem OAI.C0Absorption.correction_band_support line 253
  37. theorem OAI.C0Absorption.correction_radius_support line 261