OAI/Combinatorics/HoneycombChords/ResidualAsymptotics.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingPole_sq_ge line 18
2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.prefix_penalty_uniform line 25
3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.exponential_tail_below_power line 44
4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripJet_familyGram line 80
5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetFixedMean_bounds line 84
6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetMovingMean_bound line 98
7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physical_means_asymptotic line 108
8. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physical_means_at_minus_four line 147

   Source documentation

   The two normalized residual means have exponent -1/4.

   theorem physical_means_at_minus_four :
       ∃ a A : ℝ,0<a ∧ 0<A ∧ ∀ᶠ N : ℕ in atTop,∀ s t : ℝ,0<s → s<angle → 0<t → t<angle →
         let P:=((N:ℝ)+1)^(-1/4:ℝ)
   …

   Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.angle

9. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.parameterFamily line 168
10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.parameterFamily_interior line 170
11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_update_right line 173
12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineMoment_as_cosh line 184
13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.parameterGram_continuousOn line 193
14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedGram_det_integral line 216
15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedGram_ratio_bounds line 246
16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_measurable line 290
17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weighted_cosh_norm_integrable line 296
18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weighted_cosh_signed_integrable line 303
19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.fixedFamily_cosh_integrable line 310
20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.bounded_target_cosh_integrable line 325
21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residual_cosh_integrable line 343
22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_sq_measurable line 365
23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hOne_sq_measurable line 374
24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedMean_bounds line 393
25. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixed_physical_means_asymptotic line 409
26. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixed_physical_means_at_minus_four line 430

    Source documentation

    Normalized residuals for the two mixed families have exponent -1/4.

    theorem mixed_physical_means_at_minus_four :
        ∃ a A : ℝ,0<a ∧ 0<A ∧ ∀ᶠ N : ℕ in atTop,
          let P:=((N:ℝ)+1)^(-1/4:ℝ)
    …

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A

27. lemma OAI.CriticalHoneycomb.FiniteFunctional.pairingDomain_real_integrable line 451
28. lemma OAI.CriticalHoneycomb.FiniteFunctional.source_residual_mean line 462
29. theorem OAI.CriticalHoneycomb.FiniteFunctional.source_h_residuals_at_minus_four line 470
30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.residual_det_augment line 511
31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cThree_real line 540
32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cThree_zero line 543
33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_last line 545
34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_last_order line 549
35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extended_family line 560
36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cThree_residual_evaluation_neg line 571
37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_unitLast_column_det line 602
38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.augmented_monomial_det line 618
39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.augmented_ratio_coordinate line 634

    Source documentation

    Raising one ordered node raises the generalized interpolation error at an earlier positive point. Both the original and augmented systems have positive evaluation determinants; no monotonicity conclusion is an input.

    lemma augmented_ratio_coordinate {n : ℕ} (F : Fin n → ℝ → ℝ) (H : ℝ → ℝ)
        (hF : PositiveEvaluation F) (hA : PositiveEvaluation (Fin.lastCases H F))
        (x : Fin n → ℝ) (i : Fin n) (r a : ℝ)
        (ha : 0<a) (hax : ∀ j,a<x j) (hx : StrictMono x)
        (hr : x i ≤ r) (hy : StrictMono (Function.update x i r)) :
        (evaluationMatrix (Fin.lastCases H F) (Fin.cons a x)).det /
            (evaluationMatrix F x).det ≤
          (evaluationMatrix (Fin.lastCases H F) (Fin.cons a (Function.update x i r))).det /
            (evaluationMatrix F (Function.update x i r)).det := by
    …

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluationMatrix

40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.augmented_ratio_monotone_pos line 786
41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.augmented_ratio_monotone_zero line 799