[Merged by Bors] - feat(SpecialFunctions/Artanh): basic definition and partial equivalence

[YuvalFilmus]

Definition of artanh, and proof that it is an inverse of tanh.

---

[github-actions]

PR summary b5195ed00f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Artanh (new file)	1457

---

Declarations diff

+ abs_tanh_lt_one
+ artanh
+ artanh_bijOn
+ artanh_eq_half_log
+ artanh_eq_zero_iff
+ artanh_injOn
+ artanh_le_artanh
+ artanh_le_artanh_iff
+ artanh_lt_artanh
+ artanh_lt_artanh_iff
+ artanh_neg
+ artanh_nonneg
+ artanh_nonpos
+ artanh_pos
+ artanh_surjOn
+ artanh_tanh
+ artanh_zero
+ cosh_artanh
+ exp_artanh
+ neg_one_lt_tanh
+ sinh_artanh
+ strictMonoOn_artanh
+ strictMonoOn_one_add_div_one_sub
+ strictMonoOn_sqrt
+ tanhPartialEquiv
+ tanh_artanh
+ tanh_bijOn
+ tanh_injective
+ tanh_lt_one
+ tanh_sq_lt_one
+ tanh_surjOn

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.

---

No changes to technical debt.

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-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[SnirBroshi]

Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean uses the expression 1 / 2 * log ((1 + x) / (1 - x)) a few times (see #31487) as a stand-in for artanh.

I agree with the choice to go with sqrt so that the junk values outside of the domain will all be zero, but perhaps you should add a lemma for 1 / 2 * log ((1 + x) / (1 - x)) = artanh x for all 0 ≤ x (using Real.log_sqrt and one_div_mul_eq_div). That file should probably import this file and use the new artanh in those places.

[YuvalFilmus]

Added a theorem artanh_eq_half_log.
Perhaps the name could be improved.
I don't immediately see how to prove it for all 0 ≤ x.

[YuvalFilmus]

It is quite annoying that positivity doesn't work here (as well as elsewhere in this file).
Why is that the case?

[SnirBroshi]

I don't immediately see how to prove it for all 0 ≤ x.

Oh yes sorry I meant for all x where the thing inside the square root is non-negative.
You can extend the Ioo to Icc:

theorem artanh_eq_half_log {x : ℝ} (hx : x ∈ Icc (-1) 1) :
    artanh x = 1 / 2 * log ((1 + x) / (1 - x)) := by
  rw [artanh, log_sqrt <| div_nonneg (by grind) (by grind), one_div_mul_eq_div]

It is quite annoying that positivity doesn't work here (as well as elsewhere in this file).
Why is that the case?

I think that positivity won't do ring operations, but I'm not sure. It does know how to handle the division if you help it:

theorem artanh_eq_half_log {x : ℝ} (hx : x ∈ Icc (-1) 1) :
    artanh x = 1 / 2 * log ((1 + x) / (1 - x)) := by
  rw [artanh, log_sqrt, one_div_mul_eq_div]
  have : 0 ≤ 1 + x := by grind
  have : 0 ≤ 1 - x := by grind
  positivity

it just doesn't know how to convert -1 ≤ x to 0 ≤ 1 + x and x ≤ 1 to 0 ≤ 1 - x.

[j-loreaux]

Probably it doesn't matter, but I'll mention that if one instead chooses artanh x := 1 / 2 * log ((1 + x) / (1 - x)), then the junk values for Real.log guarantee that artanh x⁻¹ = (artanh x)⁻¹ for all x.

[SnirBroshi]

Since you asked for advice on proofs, here's how to make grind do a bit of the work for you.
In the future grind will probably be able to deduce the positivity stuff on its own too.
Though I'd probably wait for an opinion from an official Mathlib reviewer/maintainer on whether these grind proofs are better, since passing many numeric lemmas to grind is considered brittle as grind is still being worked on so its behavior isn't finalized.

[YuvalFilmus]

Added the monotonicity and positivity lemmas.

[j-loreaux]

This looks reasonable now, aside from the last comment I have. Be sure to address it and then wait for CI before merging.

bors d+

[mathlib-bors]

✌️ YuvalFilmus can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YuvalFilmus]

bors r+

[mathlib-bors]

Build failed:

• Post-Build Step

[YuvalFilmus]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step