The disc algebra is p-liquid (Lectures I-IV)
ProvedCondC.disc_liquidThe first milestone of the mission: the liquidness of the disc algebra, the key hard theorem of the paper's liquid theory, on the way to the structure sheaf theorem. The paper proves that for each 0 < p at most 1, the space O(D) of holomorphic functions on an open disc is p-liquid; from this, Theorem 1.1's identification of O(D) with convergent power series and the tensor calculus of Theorem 4.1 both flow. The theorem states: for 0 < p at most 1 and 0 < r, any complex vector space carrying the disc algebra data of radius r - a bijective, linear identification with the power-series coefficients satisfying the decay condition of Theorem 1.1 - is p-liquid.
Formalization Note p-liquidness is recorded through the interface PLiquidStructure: the designated summable families, the designated null sequences, and the unique integration functional. Profinite sets are idealized as the one-point compactification of the naturals, and the null sequences are designated abstractly, as in the paper's first formulation of liquidness: every null sequence has a unique sum.
import Mathlib import Definitions.Def_CondC_liq import Definitions.Def_CondC_geo
namespace CondC
/-! Milestone 1: the disc algebra is p-liquid. Any complex vector space
carrying the disc algebra data of radius r - elements identified
bijectively and linearly with the power series whose coefficients decay on
the disc of radius r - is p-liquid for every 0 < p at most 1. This is the
liquidness of O(D) on the way to Theorems 1.1 and 5.1. -/
theorem disc_liquid : ∀ (p r : ℝ), 0 < p → p ≤ 1 → 0 < r →
∀ (V : Type) [AddCommGroup V] [Module ℂ V],
DiscAlgebraData r V → IsPLiquid p V := by sorry
end CondC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: for every p with 0 < p at most 1 and every r with 0 < r, any complex vector space carrying the disc algebra data of radius r is p-liquid: it carries a designated space of summable families containing the Dirac families and closed under pointwise addition, subtraction, and scalar multiplication; a designated space of null sequences containing the eventually zero families and closed under pointwise addition and scalar multiplication; and an integration functional on the null sequences that evaluates Dirac families at their support point, is additive and homogeneous in the null sequence, and is uniquely determined by these requirements. No other hypotheses appear.