OAI/Analysis/HotSpots/Reciprocal.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ReciprocalKernel.pairing line 21
  2. lemma OAI.ReciprocalKernel.pairing_symm line 23
  3. lemma OAI.ReciprocalKernel.pairing_sub_smul line 27
  4. lemma OAI.ReciprocalKernel.pairing_sub_smul_right line 34
  5. lemma OAI.ReciprocalKernel.pairing_add_smul_right line 39
  6. lemma OAI.ReciprocalKernel.pairing_add_smul line 44
  7. lemma OAI.ReciprocalKernel.pairing_tendsto line 51
  8. def OAI.ReciprocalKernel.OnePositiveSquare line 60
  9. lemma OAI.ReciprocalKernel.onePositiveSquare_reverse_cauchy line 64
  10. lemma OAI.ReciprocalKernel.onePositiveSquare_of_entrywise_tendsto line 83
  11. lemma OAI.ReciprocalKernel.onePositiveSquare_isotropic_hyperplane line 106
  12. lemma OAI.ReciprocalKernel.onePositiveSquare_of_nonpos_on_kernel line 137
  13. lemma OAI.ReciprocalKernel.onePositiveSquare_rankOne_sub_psd line 155
  14. lemma OAI.ReciprocalKernel.pairing_const line 166
  15. lemma OAI.ReciprocalKernel.pairing_scale line 172
  16. lemma OAI.ReciprocalKernel.onePositiveSquare_scale line 183
  17. lemma OAI.ReciprocalKernel.onePositiveSquare_const_sub_psd line 195
  18. lemma OAI.ReciprocalKernel.normalized_complement_posSemidef line 216
  19. lemma OAI.ReciprocalKernel.posSemidef_entry_sq_le line 253
  20. lemma OAI.ReciprocalKernel.posSemidef_abs_entry_lt line 263
  21. lemma OAI.ReciprocalKernel.posSemidef_entry_pow line 273
  22. lemma OAI.ReciprocalKernel.posSemidef_of_entrywise_tendsto line 288
  23. lemma OAI.ReciprocalKernel.posSemidef_entry_resolvent line 306
  24. lemma OAI.ReciprocalKernel.onePositiveSquare_normalized_update line 320
  25. theorem OAI.ReciprocalKernel.reciprocal_rankOne_update line 373
  26. def OAI.ReciprocalKernel.bordered line 408
  27. lemma OAI.ReciprocalKernel.pairing_bordered line 411
  28. lemma OAI.ReciprocalKernel.bordered_nonpos_on_kernel line 426
  29. def OAI.ReciprocalKernel.ConditionallyNegative line 449
  30. theorem OAI.ReciprocalKernel.conditionalNegative_scaled_of_bordered line 453
  31. def OAI.ReciprocalKernel.eliminate line 486
  32. lemma OAI.ReciprocalKernel.eliminate_denominator_pos line 490
  33. lemma OAI.ReciprocalKernel.eliminate_symm line 502
  34. lemma OAI.ReciprocalKernel.eliminate_pos line 510
  35. lemma OAI.ReciprocalKernel.eliminate_bound line 519
  36. lemma OAI.ReciprocalKernel.eliminate_reciprocal line 548
  37. theorem OAI.ReciprocalKernel.finite_resolvent_of_superharmonic line 558
  38. lemma OAI.ReciprocalKernel.matrix_geometric_nonneg line 594
  39. lemma OAI.ReciprocalKernel.exists_superharmonic_of_weighted_norm_lt_one line 608
  40. theorem OAI.ReciprocalKernel.finite_resolvent line 670
  41. def OAI.ReciprocalKernel.finiteResolventKernel line 691
  42. lemma OAI.ReciprocalKernel.resolvent_eq_finiteResolventKernel line 695
  43. theorem OAI.ReciprocalKernel.finite_quadrature_reciprocal line 735
  44. def OAI.StrictHotSpots.BanachResolvent.resolvent line 759
  45. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_left line 761
  46. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_right line 764
  47. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_norm_le line 768
  48. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_identity line 778
  49. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_strong_tendsto line 784
  50. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_solution line 802
  51. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_nonneg line 808
  52. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_ge_self line 824
  53. lemma OAI.StrictHotSpots.CompactKernel.kernel_integrable line 850
  54. def OAI.StrictHotSpots.CompactKernel.kernelOp line 858
  55. lemma OAI.StrictHotSpots.CompactKernel.kernelOp_apply line 882
  56. lemma OAI.StrictHotSpots.CompactKernel.kernelOp_nonneg line 888
  57. lemma OAI.StrictHotSpots.CompactKernel.kernelOp_norm_le line 897
  58. lemma OAI.StrictHotSpots.CompactKernel.integral_comp_simpleFunc line 920
  59. def OAI.StrictHotSpots.CompactKernel.sampleOp line 936
  60. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_eq_integral line 940
  61. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_apply line 946
  62. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_nonneg line 956
  63. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_norm_le line 965
  64. def OAI.StrictHotSpots.CompactKernel.quantize line 989
  65. lemma OAI.StrictHotSpots.CompactKernel.quantize_tendsto line 991
  66. lemma OAI.StrictHotSpots.CompactKernel.integral_quantize_tendsto line 994
  67. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_strong_tendsto line 1006
  68. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_eventually_norm_le line 1013
  69. lemma OAI.ReciprocalKernel.onePositiveSquare_submatrix_sum_inl line 1035
  70. def OAI.StrictHotSpots.CompactKernel.resolvedKernel line 1056
  71. lemma OAI.StrictHotSpots.CompactKernel.sampled_reciprocal line 1062
  72. lemma OAI.StrictHotSpots.CompactKernel.continuousMap_orderClosed line 1141
  73. lemma OAI.StrictHotSpots.CompactKernel.continuous_resolvent_nonneg line 1154
  74. lemma OAI.StrictHotSpots.CompactKernel.resolvedKernel_ge line 1162
  75. lemma OAI.StrictHotSpots.CompactKernel.resolvedKernel_tendsto line 1177
  76. theorem OAI.StrictHotSpots.CompactKernel.compact_reciprocal_of_row_bound line 1193
  77. lemma OAI.StrictHotSpots.CompactKernel.integral_norm_L2_le line 1238
  78. lemma OAI.StrictHotSpots.CompactKernel.l2kernel_integrable line 1252
  79. def OAI.StrictHotSpots.CompactKernel.l2SectionOp line 1264
  80. lemma OAI.StrictHotSpots.CompactKernel.l2SectionOp_apply line 1301
  81. lemma OAI.StrictHotSpots.CompactKernel.l2SectionOp_toLp line 1307
  82. lemma OAI.StrictHotSpots.CompactKernel.l2SectionOp_nonneg line 1315
  83. def OAI.StrictHotSpots.CompactKernel.l2Op line 1324
  84. lemma OAI.StrictHotSpots.CompactKernel.l2Op_nonneg line 1327
  85. theorem OAI.StrictHotSpots.CompactKernel.exists_superharmonic line 1336
  86. def OAI.StrictHotSpots.CompactKernel.invMap line 1377
  87. def OAI.StrictHotSpots.CompactKernel.scaledKernel line 1380
  88. lemma OAI.StrictHotSpots.CompactKernel.scaledKernel_pos line 1387
  89. lemma OAI.StrictHotSpots.CompactKernel.kernelOp_scaled line 1391
  90. lemma OAI.StrictHotSpots.CompactKernel.sampleOp_scaled line 1403
  91. lemma OAI.StrictHotSpots.CompactKernel.mul_invMap line 1416
  92. lemma OAI.StrictHotSpots.CompactKernel.invMap_mul_cancel line 1421
  93. def OAI.StrictHotSpots.CompactKernel.rescaledKernel line 1426
  94. lemma OAI.StrictHotSpots.CompactKernel.scaled_row_bound line 1430
  95. def OAI.StrictHotSpots.CompactKernel.l2ResolvedKernel line 1461
  96. lemma OAI.StrictHotSpots.CompactKernel.scaled_solution line 1466
  97. lemma OAI.StrictHotSpots.CompactKernel.rescaledKernel_eq_l2ResolvedKernel line 1476
  98. lemma OAI.StrictHotSpots.CompactKernel.l2ResolvedKernel_ge line 1501
  99. lemma OAI.StrictHotSpots.CompactKernel.sampled_rescaled_reciprocal line 1516
  100. lemma OAI.StrictHotSpots.CompactKernel.rescaledKernel_tendsto line 1602
  101. theorem OAI.StrictHotSpots.CompactKernel.compact_reciprocal_of_l2_norm_lt_one line 1629
  102. lemma OAI.StrictHotSpots.CompactKernel.l2ResolvedKernel_eq_inner line 1673
  103. lemma OAI.StrictHotSpots.L2Limits.norm_sq_eq_integral_sq line 1697
  104. lemma OAI.StrictHotSpots.L2Limits.norm_toLp_sub_sq line 1703
  105. lemma OAI.StrictHotSpots.L2Limits.tendsto_toLp_of_dominated line 1711
  106. lemma OAI.StrictHotSpots.L2Limits.tendsto_L2_of_dominated line 1738
  107. lemma OAI.StrictHotSpots.CompactKernel.l2Op_ae_integral line 1755
  108. lemma OAI.StrictHotSpots.CompactKernel.l2Op_abs_domination line 1761
  109. lemma OAI.StrictHotSpots.CompactKernel.norm_l2Op_le_of_domination line 1783
  110. lemma OAI.StrictHotSpots.CompactKernel.l2Op_strong_tendsto_of_dominated line 1797
  111. lemma OAI.StrictHotSpots.BanachResolvent.resolvent_strong_tendsto_moving line 1836
  112. lemma OAI.StrictHotSpots.CompactKernel.l2Sections_tendsto_of_dominated line 1860
  113. def OAI.StrictHotSpots.CompactKernel.singularResolvedKernel line 1886
  114. lemma OAI.StrictHotSpots.CompactKernel.l2ResolvedKernel_tendsto_of_dominated line 1892
  115. lemma OAI.StrictHotSpots.CompactKernel.singularResolvedKernel_ge line 1914
  116. theorem OAI.StrictHotSpots.CompactKernel.singular_reciprocal_of_regularization line 1937
  117. def OAI.SquaredDistanceKernel.ConditionallyNegative line 2001
  118. def OAI.SquaredDistanceKernel.anchored line 2006
  119. lemma OAI.SquaredDistanceKernel.anchor_sum_identity line 2009
  120. lemma OAI.SquaredDistanceKernel.anchored_posSemidef line 2030
  121. def OAI.SquaredDistanceKernel.lifted line 2051
  122. lemma OAI.SquaredDistanceKernel.lifted_posSemidef line 2054
  123. lemma OAI.SquaredDistanceKernel.positive_kernel_realization line 2065
  124. lemma OAI.SquaredDistanceKernel.squared_distance_realization line 2078
  125. lemma OAI.SquaredDistanceKernel.injective_of_distance_positive line 2093
  126. lemma OAI.SquaredDistanceKernel.lipschitz_of_distance_bound line 2102
  127. lemma OAI.SquaredDistanceKernel.separable_lipschitz_embedding line 2116