OAI.PinchedHartogs.controlled_potential

The theorem states that there exist a function φ on the open unit ball B of ℂ² and a real constant C such that φ is real-valued and C^∞ on B, and the following three conditions hold. First, for every r in [0,1) and every complex-linear isometry U of ℂ², consider the ball automorphism-type chart ζ ↦ U((r+ζ₁)/(1+rζ₁), √(1−r²)ζ₂/(1+rζ₁)), which sends the origin to U(r,0), and let H be the complex Hessian (Levi form) of φ composed with this chart at the origin; then for every vector v in ℂ², ‖v‖² ≤ Re(Σ H_ij v_i conj(v_j)) ≤ C‖v‖², so the lower bound constant is exactly 1. Second, for the same charts, the first derivatives ∂/∂z_k and ∂/∂z̄_l and the mixed second derivative ∂²/∂z_k∂z̄_l of the Hessian entries H_ij at the origin are bounded: for all i, j, k, l in {1,2}, the sum of the moduli of those three quantities is at most C, uniformly in r and U. Third, φ has no minorant of holomorphic type: there do not exist a holomorphic function h on B and a constant K with Re h(z) ≤ K + 4 log(1/(1−|z|)) + φ(z) for all z in B. This is a statement about the existence of such a potential, and it is the defined proposition ControlledPotential, which is assumed to be admitted rather than proved here.