FourierApproximation.lean`

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

Pollaczek expansions of complete jet families

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetCombination line 18
Source documentation
Literal real complete-jet M (N jets at0 and N atL²).
```
noncomputable def twoJetCombination (N : ℕ) (a : Fin (2*N) → ℝ) (x : ℝ) : ℝ :=
…
```
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSquaredNorm line 20
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TwoJetPolynomialApproximation line 23
Source documentation
Polynomial approximation of complete jets with uniform degree and exponential error.
```
def TwoJetPolynomialApproximation : Prop :=
…
```
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_series_bound_gen line 36
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_pair_hasSum_gen line 62
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekMajorant_mul_exp_integrable line 105
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_exp_bound line 113
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_coeff_generator_full line 126
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand line 150
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_nonneg line 152
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_exp_integrable line 156
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_smul_left line 180
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_sum_left line 187
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_sub_left line 193
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_smul_left line 204
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_comm line 209
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_exp_bound line 213
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_exp_bound_sharp line 219
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_pair_integrable line 230
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_generator_integrable line 235
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekGenerator_pair_integrable line 243
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTruncation line 258
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTruncation_eval line 260
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTruncation_bounds line 267
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTruncation_tendsto line 274
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetSech_square_integrable line 278
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTruncation_L2_tendsto line 299
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekFinite line 331
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_pollaczekFinite line 333
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_pollaczekFinite_integrable line 341
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_pollaczekFinite line 346
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekFinite_coeff line 352
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekFinite_pair_integrable line 357
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekFinite_norm line 363
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_sub_left line 372
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_difference_norm line 377
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_projection_squared_error line 392
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_bessel line 405
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPollaczekFinite line 420
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenPollaczekFinite_polynomial line 422
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_evenPollaczekFinite line 428
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_evenFinite line 433
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_pair_integrable line 441
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_pair line 446
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_coeff line 453
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_square_integrable line 460
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_norm line 466
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.even_projection_error line 473
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.even_projection_minimal line 482
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.even_projection_bessel line 492
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetTruncation_degree line 509
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetSech_pair_integrable line 514
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenSech_squaredNorm line 526
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetSech_norm_integrable line 535
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJetSech_parseval_residual line 545
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetCombination line 573
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetTruncation line 575
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetTruncation_eval line 577
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetTruncation_degree line 580
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetCombination_continuous line 586
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetTruncation_error_bound line 591
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetTruncation_L2_tendsto line 604
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetSech_pair_integrable line 638
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetSech_norm_integrable line 650
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteJetSech_parseval_residual line 671
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCoshPolynomial line 700
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetSinhPolynomial line 705
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetPolynomial_degrees line 710
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_polynomials line 736
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMoment line 762
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMoment_continuous line 763
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.power_exp_bound line 765
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMoment_bound line 771
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMoment_pair_integrable line 778
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff_moment_integrable line 785
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMomentCoefficient line 800
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMomentCoefficient_zero line 802
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczek_coeff_recurrence line 806
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMomentCoefficient_succ line 812
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMomentPolynomial line 828
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMomentPolynomial_degree line 832
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorMomentCoefficient_polynomial line 851
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorPolynomial line 869
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorPolynomial_sum line 870
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorPolynomial_pair_integrable line 879
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorPolynomialCoefficient line 894
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorPolynomialCoefficient_degree line 896
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generatorPolynomial_coefficient line 901
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generator_even_sum line 925
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generator_odd_sum line 931
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_generator_polynomials line 937
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_add_right line 959
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_evenCoefficient line 970
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSech_pair_integrable line 1000
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomialSech_coefficient_zero line 1005
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJet_zeroLabel_polynomial line 1012
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJet_zeroLabel_coefficient line 1018
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJet_zeroLabel_pair_integrable line 1023
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernelJet_arctan_pair_integrable line 1027
def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination line 1041
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination_coefficient line 1043
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination_finite line 1096
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_bounds line 1101
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_norm_integrable line 1114
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_pair_integrable line 1120
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_parseval_residual line 1126
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.label_margin_exists line 1134
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.arctan_label_margin line 1139
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenProjection_coefficient_le_one line 1156
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenProjection_hasSum line 1167
lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenProjection_exponential_error line 1178