OAI/Combinatorics/HoneycombChords/ObliqueProjection.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Bilinear Gram projection onto the finite interpolation space and its residuals.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.complexInsertedFamily line 18
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.complexInsertedFamily_low line 21
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.complexInsertedFamily_high line 31
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.beta_angle_mem_M line 43
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.beta_zero_mem_M line 55
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.complexInsertedFamily_span line 65
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.fixedFamily_span line 116
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.mixedFamily_span line 127
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_sub line 149
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_add line 157
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_smul line 163
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_comm line 168
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.comm line 174
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.sub line 180
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.finset_sum line 184
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_finset_sum line 193
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.PairingIntegrable.span_left line 203
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_annihilates_span line 212
  19. def OAI.CriticalHoneycomb.FiniteFunctional.fBasis line 234
  20. def OAI.CriticalHoneycomb.FiniteFunctional.gBasis line 235
  21. def OAI.CriticalHoneycomb.FiniteFunctional.pairingMatrix line 236
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingKernel_ofReal line 239
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairing_ofReal line 246
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.fBasis_gBasis_integrable line 255
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingMatrix_eq line 263
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingMatrix_det_ne_zero line 268
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.fBasis_span line 274
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.gBasis_span line 276
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.fBasis_density_integrable line 279
  30. def OAI.CriticalHoneycomb.FiniteFunctional.projectionCoefficients line 298
  31. def OAI.CriticalHoneycomb.FiniteFunctional.obliqueProjection line 300
  32. def OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual line 302
  33. def OAI.CriticalHoneycomb.FiniteFunctional.InPairingDomain line 304
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.projection_mem line 306
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.projection_integrable line 311
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.projection_pairing line 317
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.residual_pairing_zero line 327
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.residual_density_pairing_zero line 331
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.domain_density_integrable line 340
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.projection_density_integrable line 348
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.projection_unique line 352
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.real_projection_coefficients line 382
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.projection_ofReal line 408
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.residual_ofReal_mean line 421
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosh_parameter_norm line 446
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosh_pair_continuousOn line 453
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosh_pair_fubini line 467
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.colDet_integral line 495