OAI/Combinatorics/HoneycombChords/JetApproximation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integerGapProduct line 18
2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integerGapProduct_erase line 53
3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integer_lagrange_basis_bound line 61
4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integer_polynomial_bound line 82
5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.integer_polynomial_exponential_bound line 125

   Source documentation

   Quantitative Lagrange bound, with an arbitrarily small exponential instead of a Stirling asymptotic. Used on the literal q^j p(j) Pollaczek tails.

   lemma integer_polynomial_exponential_bound (n : ℕ) (a x B α : ℝ)
       (ha : 0 ≤ a) (hx : a+(n:ℝ) ≤ x) (hB : 0 ≤ B) (hα : 0<α)
       (P : Polynomial ℝ) (hP : P.natDegree ≤ n)
       (hvalues : ∀ i : Fin (n+1),|P.eval (a+(i:ℝ))| ≤ B) :
       |P.eval x| ≤ B*(2/α)^n*Real.exp (α*x) := by
   …

6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.exp_power_bound line 137
7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.exponential_polynomial_sample_tail line 151

   Source documentation

   Exponential coefficient decay from bounds at consecutive sample points.

   lemma exponential_polynomial_sample_tail {q : ℝ} (hq0 : 0<q) (hq1 : q<1) :
       ∃ D γ : ℝ,0<D ∧ 0<γ ∧ ∀ N : ℕ,0<N → ∀ P : Polynomial ℝ,P.natDegree<N →
         (∀ i : Fin N,|P.eval (N+(i:ℝ))| ≤ (q^ (2*N))⁻¹) →
         ∀ j : ℕ,(D*(N:ℝ) ≤ j) → |q^j*P.eval (j:ℝ)| ≤ Real.exp (-γ*(j:ℝ)) := by
   …

   Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D

8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_exponential_coefficients line 198

   Source documentation

   The uniform coefficient decay asserted in the approximation paragraph, for the literal complete zero/L² jet space and the explicit sech weight.

   lemma completeJetSech_exponential_coefficients {u : ℝ} (hu : |u|<1) (hu0 : u≠0) :
       ∃ D γ : ℝ,0<D ∧ 0<γ ∧ ∀ N:ℕ,0<N → ∀ a c:Fin N→ℝ,
         symmetricSechPair (completeJetCombination N ((2*Real.arctan u)^2) a c)
           (completeJetCombination N ((2*Real.arctan u)^2) a c)≤1 →
         ∀ j:ℕ,D*(N:ℝ)≤j →
           |symmetricSechPair (fun p=>pollaczekCoeff p (2*j)) (completeJetCombination N ((2*Real.arctan u)^2) a c)|≤
             Real.exp (-γ*(j:ℝ)) := by
   …

   Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pollaczekCoeff

9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_projection_approximation line 233
10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_scale_right line 260
11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination_scale line 273
12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetCombination_split line 287
13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sum_fin_geometric_le line 314
14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_pointwise_bound line 326
15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_spatial_tail line 353
16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_self_nonneg line 395
17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPair_difference_integrable line 398
18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_local_mass line 408
19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.exponential_nat_uniform_small line 450
20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.spatial_exponential_constant line 469
21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.exponential_relative_constant line 495
22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetSech_concentration line 522
23. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalfNorm line 572
24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechPairIntegrand_even line 573
25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalf_integrable line 576
26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalf_le_sech line 588
27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalf_lower_local line 601
28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledStripDensity_measurable line 623
29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scaledStripDensity_pos line 626
30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination_continuous line 637
31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination_even line 644
32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetCombination_smul line 647
33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_continuous line 651
34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_even line 655
35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evenFinite_polynomial_degree line 657
36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.symmetricSechPair_smul_both line 661
37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalfNorm_smul line 665
38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.normalizedJetWeightedApproximation line 679
39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalfNorm_nonneg line 741
40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.relativeJetWeightedApproximation line 745
41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedHalfNorm_scale line 804
42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripApproximation_scale_parameters line 813
43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.completeJetStripApproximation line 837
44. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetPolynomialApproximation line 878

    Source documentation

    Polynomial approximation for the strip weight and complete nodal jet space.

    theorem twoJetPolynomialApproximation : TwoJetPolynomialApproximation := by
    …

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TwoJetPolynomialApproximation