Research proof index

f₄ transforms under T as f₄|T = f₃. Proof outline: 1. (serre_D 2 H₄)|[4]T = serre_D 2 (H₄|[2]T) = serre_D 2 H₃ 2. (H₄(2H₂ + H₄))|[4]T = H₃(2(-H₂) + H₃) = H₃(H₃ - 2H₂) Using Jacobi H₃ = H₂ + H₄: H₃ - 2H₂ = H₄ - H₂ 3. f₄|[4]T = serre_D 2 H₃ + (1/6)H₃(H₃ - 2H₂) But H₂² - H₄² = (H₂ - H₄)(H₂ + H₄) = (H₂ - H₄)H₃ So (1/6)(H₂² - H₄²) = -(1/6)H₃(H₄ - H₂) = -(1/6)H...

f₄ tends to 0 at infinity. Proof: f₄ = serre_D 2 H₄ + (1/6)H₄(2H₂ + H₄) serre_D 2 H₄ = D H₄ - (1/6)E₂ H₄ → 0 - (1/6)11 = -1/6 (since H₄ → 1, E₂ → 1) H₄(2H₂ + H₄) → 1*(0 + 1) = 1 So f₄ → -1/6 + (1/6)*1 = 0.

Division of MDifferentiable functions on ℍ is MDifferentiable, when the denominator is everywhere nonzero.

If g(t₀) = 0 and deriv g t₀ < 0, then g is negative shortly after t₀.

If g is continuous on (0, ∞), positive for t ≥ t₀, and has strictly negative derivative at any zero in (0, t₀), then g is positive on all of (0, ∞).

The Serre derivative of a bounded holomorphic function is bounded at infinity. serre_D k f = D f - (k/12)·E₂·f. Both terms are bounded: - D f is bounded by D_isBoundedAtImInfty_of_bounded - (k/12)·E₂·f is bounded since E₂ and f are bounded