feat(Analysis/SpecialFunctions): BinetFormula part 3

[jonwashburn]

PR 3 towards Hadamard Factorization
Co-authored with Matteo Cipollina (matteo.cipollina@yahoo.it)

• depends on: feat(Analysis/SpecialFunctions): BinetFormula part 2 #34339

---

[github-actions]

PR summary 18ef4ef4f3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Gamma.BinetKernel (new file)	2495
Mathlib.Analysis.SpecialFunctions.Gamma.BinetFormula (new file)	2550

---

Declarations diff

+ Gamma_bound_one_two'
+ Gamma_le_one_of_mem_Icc
+ J
+ J_eq_integral
+ J_eq_stirlingSeries_add_remainder
+ J_norm_le_re
+ J_norm_le_real
+ J_well_defined
+ K
+ K_eq_alt
+ K_eq_alt'
+ K_nonneg
+ K_pos
+ Ktilde
+ Ktilde_bdd
+ Ktilde_ge_one_div_twelve_mul_exp_neg_div_twelve
+ Ktilde_le
+ Ktilde_lt
+ Ktilde_mul_exp_le
+ Ktilde_mul_one_sub_exp_eq_integral
+ Ktilde_nonneg
+ Ktilde_pos
+ Ktilde_zero
+ R
+ R_eq_re_J
+ R_sub_R_add_one
+ Real_log_Gamma_eq_Binet
+ bernoulliReal
+ continuousOn_Ktilde_Ioi
+ continuous_Ktilde
+ differentiableOn_gAux
+ differentiableOn_gAux'
+ differentiableOn_gAux''
+ differentiableOn_robbinsAux
+ differentiableOn_robbinsAux'
+ differentiableOn_robbinsAux''
+ differentiableOn_robbinsAux'''
+ eq_of_tendsto_atTop_of_add_one
+ exp_mul_one_sub_lt_one
+ exp_sub_one_pos
+ f
+ f_at_one
+ f_deriv
+ f_deriv'
+ f_deriv_pos
+ f_nonneg
+ f_one_pos
+ f_zero
+ gAux
+ gAux'
+ gAux''
+ gAux'''
+ gAux'''_nonneg
+ gAux'''_pos
+ gAux''_nonneg
+ gAux''_pos
+ gAux''_zero
+ gAux'_nonneg
+ gAux'_pos
+ gAux'_zero
+ gAux_nonneg
+ gAux_pos
+ gAux_zero
+ hasDerivAt_gAux
+ hasDerivAt_gAux'
+ hasDerivAt_gAux''
+ hasDerivAt_robbinsAux
+ hasDerivAt_robbinsAux'
+ hasDerivAt_robbinsAux''
+ hasDerivAt_robbinsAux'''
+ hasDerivAt_robbinsPoly
+ integrable_Ktilde_exp
+ integrable_Ktilde_exp_complex
+ integrable_Ktilde_mul_exp_neg_mul
+ integrable_const_mul_exp
+ integral_exp_neg_mul_Ioi
+ log_Gamma_real_eq
+ log_Gamma_real_eq_of_R_eq_re_J
+ monotoneOn_of_deriv_nonneg_Ici
+ nonneg_of_deriv_nonneg_Ici
+ norm_Gamma_le_Gamma_re
+ norm_Gamma_le_one
+ norm_Ktilde_mul_exp
+ one_div_cast_sub_le_two_div_cast
+ re_J_eq_integral_Ktilde
+ re_J_le_one_div_twelve
+ re_J_lt_one_div_twelve
+ re_J_pos
+ re_J_sub_re_J_add_one
+ robbinsAux
+ robbinsAux'
+ robbinsAux''
+ robbinsAux'''
+ robbinsAux''''
+ robbinsAux''''_nonneg
+ robbinsAux'''_nonneg
+ robbinsAux'''_zero
+ robbinsAux''_nonneg
+ robbinsAux''_zero
+ robbinsAux'_nonneg
+ robbinsAux'_zero
+ robbinsAux_nonneg
+ robbinsAux_zero
+ robbinsPoly
+ robbinsPoly'
+ robbinsPoly'_pos
+ robbinsPoly_pos
+ stirlingMainReal
+ stirlingMainReal_add_one_sub
+ stirlingRemainder
+ stirlingRemainder_zero_bound
+ stirlingRemainder_zero_bound_real
+ stirlingSeries
+ stirlingTerm
+ tendsto_Ktilde_zero
+ tendsto_R_atTop
+ tendsto_exp_sub_one_div
+ tendsto_exp_taylor3_div_cube
+ tendsto_f_div_cube
+ tendsto_re_J_atTop

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.42)

Current number	Change	Type
4	1	maxHeartBeats modifications
6	1	large files

Current commit a3924e45a5
Reference commit 18ef4ef4f3

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Analysis/SpecialFunctions): BinetFormula part 2 #34339
  By Dependent Issues (🤖). Happy coding!