MagneticInverseGenerator.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The inverse-mean generator identities. The hypotheses are the ordinary backward Gaussian derivative identities, and the inverse-coordinate form follows from the proved implicit-bias variation rule.

lemma OAI.InvariantIsing.inverse_curvature_generator line 15
lemma OAI.InvariantIsing.inverse_continuation_generator line 27
lemma OAI.InvariantIsing.inverse_diffusion_second line 42
Source documentation
The zeroth-order coefficient of the twice differentiated inverse continuation equation only needs the ratio of fourth and second ordinary derivatives: the apparent square of the third derivative cancels.
```
lemma inverse_diffusion_second {q r w : ℝ} (hq : q ≠ 0) :
    2 * (r / q) ^ 2 + 2 * q * (w / q ^ 2 - r ^ 2 / q ^ 3) = 2 * w / q := by
…
```