OAI/Combinatorics/HoneycombChords/ParameterJets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_eq_beta_square line 18
2. def OAI.CriticalHoneycomb.FiniteFunctional.composeCoeff line 26
3. lemma OAI.CriticalHoneycomb.FiniteFunctional.composeCoeff_smooth line 33
4. lemma OAI.CriticalHoneycomb.FiniteFunctional.composeCoeff_zero line 43
5. lemma OAI.CriticalHoneycomb.FiniteFunctional.composeCoeff_diagonal line 53
6. lemma OAI.CriticalHoneycomb.FiniteFunctional.beta_square_hasDerivAt line 64
7. lemma OAI.CriticalHoneycomb.FiniteFunctional.C_parameter_jet_expansion line 74
8. lemma OAI.CriticalHoneycomb.FiniteFunctional.parameter_jet_span line 110
9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_eq_jet line 131
10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A_eq_jet_fun line 134
11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cos_alpha_pos line 137
12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_ordinary_pair_integrable line 143
13. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_ordinary_coefficient_lower line 152

    Source documentation

    Separated-knot coefficient estimate for the actual cosine families. The Gram invertibility here will be discharged by the sorted positive jet flag.

    theorem sech_ordinary_coefficient_lower (N : ℕ) (q : Fin (2*N) → ℝ) (u t : ℝ)
        (hq : ∀ i,0 ≤ q i ∧ q i ≤ angle) (hu : 0 ≤ u ∧ u ≤ angle) (ht : 0 ≤ t ∧ t ≤ angle)
        (hinj : Function.Injective (Fin.lastCases t q))
        (hd : (familyGram (sechProbDensity (3*angle))
          (fun i : Fin (2*N+1) ↦ cosineKernelJet 0 0 ((Fin.lastCases u q i)^2))
          (fun i : Fin (2*N+1) ↦ cosineKernelJet 0 0 ((Fin.lastCases t q i)^2))).det≠0) :
        1/(68*Real.pi*Real.sqrt ((N:ℝ)+1))  ≤  -meanResidualRatio (sechProbDensity (3*angle))
          (fun i : Fin (2*N+1) ↦ cosineKernelJet 0 0 ((Fin.lastCases u q i)^2))
          (fun i : Fin (2*N+1) ↦ cosineKernelJet 0 0 ((Fin.lastCases t q i)^2))
          (cosineKernelJet 0 0 ((3*angle/2)^2)) 0 := by
    …

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechProbDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio

14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_approximate_coefficient_lower line 235
15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetFamily_as_newton line 305
16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonFamilyGram_det_ne_zero line 314
17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.tendsto_jet_meanResidualRatio line 339
18. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sech_confluent_coefficient_lower line 377

    Source documentation

    Quantitative coefficient noncancellation for the exact two-cluster jet flags under the sech comparison measure. The systems remain nonsymmetric.

    theorem sech_confluent_coefficient_lower (N : ℕ) {u t : ℝ}
        (hu : 0<u) (huL : u<angle) (ht : 0<t) (htL : t<angle) :
        1/(68*Real.pi*Real.sqrt ((N:ℝ)+1)) ≤
          -meanResidualRatio (sechProbDensity (3*angle))
            (fun i : Fin (2*N+1) ↦ cosineKernelJet (nodalOrder (interiorKnotLabels N u) i) 0
              (interiorKnotLabels N u i))
            (fun i : Fin (2*N+1) ↦ cosineKernelJet (nodalOrder (interiorKnotLabels N t) i) 0
              (interiorKnotLabels N t i)) (cosineKernelJet 0 0 ((3*angle/2)^2)) 0 := by
    …

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechProbDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnotLabels