OAI/Combinatorics/HoneycombChords/CauchyResidual.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Cauchy interpolation residual formulas and their quantitative integral lower bounds.

  1. def OAI.Honeycomb370.cauchyDen line 13
  2. def OAI.Honeycomb370.cauchyDenExcept line 15
  3. def OAI.Honeycomb370.cauchyNumerator line 17
  4. lemma OAI.Honeycomb370.cauchyDen_eval line 20
  5. lemma OAI.Honeycomb370.cauchyDenExcept_eval line 22
  6. lemma OAI.Honeycomb370.cauchyNumerator_one line 24
  7. lemma OAI.Honeycomb370.cauchyDen_split line 26
  8. lemma OAI.Honeycomb370.cauchyNumerator_degree line 29
  9. theorem OAI.Honeycomb370.cauchy_residual_numerator line 54
  10. def OAI.Honeycomb370.sechErrorPositive line 88

    Source documentation

    Negative of the exact Cauchy-model transform residual at v=-s. The 2N common nodes are not symmetrized with the final distinct F/G nodes.

    noncomputable def sechErrorPositive (N : ℕ) (q : Fin (2*N) → ℝ) (u t s : ℝ) : ℝ :=
…
  11. lemma OAI.Honeycomb370.sechErrorPositive_lower line 91
  12. lemma OAI.Honeycomb370.cauchy_scale_power_lower line 123
  13. lemma OAI.Honeycomb370.sechErrorPositive_tail_lower line 144
  14. def OAI.Honeycomb370.cauchyEvalFunctional line 164
  15. lemma OAI.Honeycomb370.cauchy_boundary_identity line 167
  16. lemma OAI.Honeycomb370.cauchy_quadratic_integrable line 178
  17. lemma OAI.Honeycomb370.cauchyEval_on_kernel line 190
  18. lemma OAI.Honeycomb370.sechErrorPositive_bounds line 214
  19. def OAI.Honeycomb370.sechErrorIntegrand line 248
  20. lemma OAI.Honeycomb370.sechErrorIntegrand_integrable line 251
  21. theorem OAI.Honeycomb370.sechModel_integral_lower line 287
  22. def OAI.Honeycomb370.cauchyResidual line 344
  23. lemma OAI.Honeycomb370.cauchyResidual_fraction line 347
  24. lemma OAI.Honeycomb370.cauchyNumerator_zero_of_orth line 364
  25. lemma OAI.Honeycomb370.cauchyResidual_product line 374
  26. lemma OAI.Honeycomb370.cauchyResidual_common_negative line 384
  27. lemma OAI.Honeycomb370.cauchyResidual_eval line 432
  28. theorem OAI.Honeycomb370.cauchyResidual_zero_lower line 466

    Source documentation

    Quantitative evaluation at zero of the exact nonsymmetric Cauchy residual.

    theorem cauchyResidual_zero_lower (N : ℕ) (q : Fin (2*N) → ℝ) (u t : ℝ)
    (c : Fin (2*N+1) → ℝ) (hq : ∀ i,0≤q i ∧ q i≤1/2) (hu : 0≤u ∧ u≤1/2)
    (ht : 0≤t ∧ t≤1/2) (hinj : Function.Injective (Fin.lastCases t q))
    (horth : ∀ j,1/(1-Fin.lastCases t q j)=
      ∑ i,c i/(1-Fin.lastCases u q i*Fin.lastCases t q j)) :
    1/(68*Real.pi*Real.sqrt ((N:ℝ)+1)) ≤
      -(1/Real.sqrt 2-∑ i,c i/Real.sqrt (1+Fin.lastCases u q i)) := by
…