Proved counterparts of Statement.lean

This module imports all five mathematical libraries and proves the local statements below. Its elementary definitions are explicit, so their meanings can be inspected independently of the development. The upstream statement and audit guide describe the separate comparator submission at the pinned source revision; this import does not maintain that upstream comparison.

def PalomarSnapshot.simplex {ι : Type u_1} [Fintype ι] : Set (ι → ℝ)

Nonnegative coordinates summing to one: the ambient standard simplex.

Equations

• PalomarSnapshot.simplex = {u : ι → ℝ | (∀ (i : ι), 0 ≤ u i) ∧ ∑ i : ι, u i = 1}

def PalomarSnapshot.interior {ι : Type u_1} [Fintype ι] : Set (ι → ℝ)

The positive-coordinate part of the simplex.

Equations

• PalomarSnapshot.interior = {u : ι → ℝ | u ∈ PalomarSnapshot.simplex ∧ ∀ (i : ι), 0 < u i}

noncomputable def PalomarSnapshot.chart {ι : Type u_1} [Fintype ι] (i : ι) (x : { j : ι // j ≠ i } → ℝ) : ι → ℝ

Recover coordinate i as one minus the sum of the remaining coordinates.

Equations

• PalomarSnapshot.chart i x = (Equiv.funSplitAt i ℝ).symm (1 - ∑ j : { j : ι // j ≠ i }, x j, x)

noncomputable def PalomarSnapshot.simplexMeasure {ι : Type u_1} [Fintype ι] : MeasureTheory.Measure (ι → ℝ)

Coordinate Lebesgue measure on the whole sum-one hyperplane; zero for no coordinates. There is no Euclidean square-root-of-cardinality factor in this normalization.

Equations

• PalomarSnapshot.simplexMeasure = if h : Nonempty ι then MeasureTheory.Measure.map (PalomarSnapshot.chart (Classical.choice h)) MeasureTheory.volume else 0

noncomputable def PalomarSnapshot.density {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (u : ι → ℝ) : ℂ

Gamma-regularized complex density, zero outside the positive simplex.

Equations

• PalomarSnapshot.density b u = PalomarSnapshot.interior.indicator (fun (u : ι → ℝ) => ∏ i : ι, ↑(u i) ^ (b i - 1) / Complex.Gamma (b i)) u

noncomputable def PalomarSnapshot.average {ι : Type u_1} [Fintype ι] (b z : ι → ℂ) (f : ℂ → ℂ) : ℂ

The native Gamma-regularized average of f at the affine combination of the nodes. Its simplex density is ∏ i, uᵢ ^ (bᵢ - 1) / Gamma bᵢ. On the convergence domain, the ordinary normalized Dirichlet average is Gamma (∑ i, b i) * average b z f; see complexDirichletIntegral_eq_gamma_mul. The continuation theorem below extends the regularized average to all parameters. This totalized native integral is not itself that continuation outside convergence.

Equations

• PalomarSnapshot.average b z f = ∫ (u : ι → ℝ) in PalomarSnapshot.simplex, PalomarSnapshot.density b u * f (∑ i : ι, ↑(u i) * z i) ∂PalomarSnapshot.simplexMeasure

noncomputable def PalomarSnapshot.realDirichlet {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : MeasureTheory.Measure (ι → ℝ)

Real Dirichlet distribution: the normalized power density on the positive simplex. Its probability interpretation requires positive parameters and a nonempty index type.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PalomarSnapshot.coordDeriv {ι : Type u_1} (i : ι) (f : (ι → ℂ) → ℂ) (z : ι → ℂ) : ℂ

Ordinary coordinate differentiation, holding all other coordinates fixed.

Equations

• PalomarSnapshot.coordDeriv i f z = deriv (fun (w : ℂ) => f (Function.update z i w)) (z i)

theorem PalomarSnapshot.gamma_shift (z : ℂ) (n : ℕ) : (Complex.Gamma z)⁻¹ = Polynomial.eval z (ascPochhammer ℂ n) * (Complex.Gamma (z + ↑n))⁻¹

Reciprocal Gamma shift, including its zeros at nonpositive integers.

theorem PalomarSnapshot.vandermonde {A : Type u_2} [CommSemiring A] (r s : A) (n : ℕ) : Polynomial.eval (r + s) (ascPochhammer A n) = ∑ ij ∈ Finset.antidiagonal n, ↑(n.choose ij.1) * (Polynomial.eval r (ascPochhammer A ij.1) * Polynomial.eval s (ascPochhammer A ij.2))

Chu–Vandermonde for rising factorials over any commutative semiring.

theorem PalomarSnapshot.holomorphic_analytic {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set E} {f : E → F} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) : AnalyticOnNhd ℂ f U

Complex Fréchet differentiability on an open finite-dimensional domain implies analyticity.

theorem PalomarSnapshot.osgood {ι : Type u_1} [Fintype ι] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (ι → ℂ)} {f : (ι → ℂ) → F} (hU : IsOpen U) (hc : ContinuousOn f U) (hf : ∀ z ∈ U, ∀ (i : ι), AnalyticAt ℂ (fun (w : ℂ) => f (Function.update z i w)) (z i)) : AnalyticOnNhd ℂ f U

Joint continuity and separate holomorphy imply joint analyticity (not Hartogs without continuity).

theorem PalomarSnapshot.cauchy_derivatives {c : ℂ} {r : ℝ} {f : ℂ → ℂ} (hf : DiffContOnCl ℂ f (Metric.ball c r)) (hr : 0 < r) (n : ℕ) {w : ℂ} (hw : w ∈ Metric.ball c r) : iteratedDeriv n f w = ↑n.factorial * (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (s : ℂ) in C(c, r), (s - w) ^ (-(↑n + 1)) * f s

Cauchy's formula for every derivative at any interior point, requiring only boundary continuity.

theorem PalomarSnapshot.simplex_chart_independent {ι : Type u_1} [Fintype ι] [Nonempty ι] (i : ι) : simplexMeasure = MeasureTheory.Measure.map (chart i) MeasureTheory.volume

Every omitted-coordinate chart defines the same ambient measure.

theorem PalomarSnapshot.simplex_monomial {ι : Type u_1} [Fintype ι] [Nonempty ι] (m : ι → ℕ) : ∫ (u : ι → ℝ) in simplex, ∏ i : ι, u i ^ m i ∂simplexMeasure = ↑(∏ i : ι, (m i).factorial) / ↑(Fintype.card ι + ∑ i : ι, m i - 1).factorial

Simplex monomial integral with coordinate-volume normalization, including the singleton case.

theorem PalomarSnapshot.complex_beta_integral {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : ∀ (i : ι), 0 < (b i).re) : (∏ i : ι, Complex.Gamma (b i)) / Complex.Gamma (∑ i : ι, b i) = ∫ (u : ι → ℝ) in simplex, ∏ i : ι, ↑(u i) ^ (b i - 1) ∂simplexMeasure

Absolutely convergent multivariate beta integral; each parameter has positive real part.

theorem PalomarSnapshot.dirichlet_probability {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : ∀ (i : ι), 0 < b i) : MeasureTheory.IsProbabilityMeasure (realDirichlet b)

Positive real parameters on a nonempty simplex define a probability measure.

theorem PalomarSnapshot.dirichlet_moments {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : ∀ (i : ι), 0 < b i) (m : ι → ℕ) : ∫ (u : ι → ℝ), ∏ i : ι, u i ^ m i ∂realDirichlet b = (∏ i : ι, Polynomial.eval (b i) (ascPochhammer ℝ (m i))) / Polynomial.eval (∑ i : ι, b i) (ascPochhammer ℝ (∑ i : ι, m i))

All natural mixed moments of the real Dirichlet distribution.

theorem PalomarSnapshot.dirichlet_aggregation {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] {q : ι → κ} (hq : Function.Surjective q) {b : ι → ℝ} (hb : ∀ (i : ι), 0 < b i) : MeasureTheory.MeasurePreserving (⇑(FunOnFinite.linearMap ℝ ℝ q)) (realDirichlet b) (realDirichlet ((FunOnFinite.linearMap ℝ ℝ q) b))

Summing coordinates in surjective blocks sums the corresponding Dirichlet parameters.

theorem PalomarSnapshot.joint_average_continuation {ι : Type u_1} [Fintype ι] {D : Set ℂ} (hD : IsOpen D) (hconv : Convex ℝ D) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f D) : ∃ (G : (ι → ℂ) × (ι → ℂ) → ℂ), AnalyticOnNhd ℂ G {p : (ι → ℂ) × (ι → ℂ) | Set.range p.2 ⊆ D} ∧ ∀ (z : ι → ℂ), Set.range z ⊆ D → ∀ (b : ι → ℂ), (∀ (i : ι), 0 < (b i).re) → G (b, z) = average b z f

The Gamma-regularized continuation assertion of Carlson 1977, 6.3-6, on a convex open scalar domain. The extension is entire in the Dirichlet parameters and jointly analytic with the nodes; native agreement is asserted only when every parameter has positive real part.

noncomputable def PalomarSnapshot.regR {ι : Type u_2} [Fintype ι] (t : ℂ) (b z : ι → ℂ) : ℂ

Gamma-regularized Carlson R on the principal slit domain. The solution supplies its construction; r_joint and r_native fix its mathematical meaning.

Equations

• PalomarSnapshot.regR t b z = DirichletTransform.regCarlsonRSlit t b z

@[reducible, inline]

noncomputable abbrev PalomarSnapshot.regL {ι : Type u_1} [Fintype ι] (t : ℂ) (b z : ι → ℂ) : ℂ

Gamma-regularized Carlson L is the exponent derivative of the same R-function.

Equations

• PalomarSnapshot.regL t b z = deriv (fun (s : ℂ) => PalomarSnapshot.regR s b z) t

theorem PalomarSnapshot.r_joint {ι : Type u_1} [Fintype ι] : AnalyticOnNhd ℂ (fun (p : Option (ι ⊕ ι) → ℂ) => regR (p none) (fun (i : ι) => p (some (Sum.inl i))) fun (i : ι) => p (some (Sum.inr i))) {p : Option (ι ⊕ ι) → ℂ | ∀ (i : ι), p (some (Sum.inr i)) ∈ Complex.slitPlane}

Carlson 6.8-2: joint holomorphy in all exponents, all Dirichlet parameters, and slit-plane nodes.

theorem PalomarSnapshot.r_native {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : ∀ (i : ι), 0 < (b i).re) (hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane) : regR t b z = average b z fun (w : ℂ) => w ^ t

R equals its native power average when the entire node convex hull stays in the slit plane.

theorem PalomarSnapshot.r_euler {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : ∀ (i : ι), z i ∈ Complex.slitPlane) : regR t b z = (∏ i : ι, z i ^ (-b i)) * regR (-∑ i : ι, b i - t) b fun (i : ι) => (z i)⁻¹

Carlson 6.8-3: Euler inversion on all slit-plane nodes and all complex parameters.

theorem PalomarSnapshot.r_euler_poisson {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : ∀ (i : ι), z i ∈ Complex.slitPlane) (i j : ι) : (z i - z j) * coordDeriv i (coordDeriv j (regR t b)) z + b i * coordDeriv j (regR t b) z - b j * coordDeriv i (regR t b) z = 0

Euler–Poisson on the full slit domain, including repeated indices and coincident nodes.

theorem PalomarSnapshot.r_first_quadratic (t β x y : ℂ) (hx : 0 < x.re) (hy : 0 < y.re) : regR (2 * t) ![β, β] ![x, y] = 2 ^ (1 - 2 * β) * ↑√Real.pi * (Complex.Gamma β)⁻¹ * regR t ![β + t, 1 / 2 - t] ![((x + y) / 2) ^ 2, x * y]

First quadratic transformation (6.9): all t, beta, with positive-real-part unsquared variables.

theorem PalomarSnapshot.r_second_quadratic (t β x y : ℂ) (hx : 0 < x.re) (hy : 0 < y.re) : regR t ![β, β] ![x ^ 2, y ^ 2] = 2 ^ (1 - 2 * β) * ↑√Real.pi * (Complex.Gamma β)⁻¹ * regR t ![2 * β + t, 1 / 2 - β - t] ![((x + y) / 2) ^ 2, x * y]

Second quadratic transformation (6.10): squared and transformed nodes need not have positive real parts.

theorem PalomarSnapshot.l_joint {ι : Type u_1} [Fintype ι] : AnalyticOnNhd ℂ (fun (p : Option (ι ⊕ ι) → ℂ) => regL (p none) (fun (i : ι) => p (some (Sum.inl i))) fun (i : ι) => p (some (Sum.inr i))) {p : Option (ι ⊕ ι) → ℂ | ∀ (i : ι), p (some (Sum.inr i)) ∈ Complex.slitPlane}

Carlson 1987, (2.1): L is jointly holomorphic on the same full parameter and slit-node domain.

theorem PalomarSnapshot.l_native {ι : Type u_1} [Fintype ι] (t : ℂ) {b z : ι → ℂ} (hb : ∀ (i : ι), 0 < (b i).re) (hz : (convexHull ℝ) (Set.range z) ⊆ Complex.slitPlane) : regL t b z = average b z fun (w : ℂ) => w ^ t * Complex.log w

L equals the native power-logarithm average on the hull-admissible slit domain.

theorem PalomarSnapshot.l_exponent_derivative {ι : Type u_1} [Fintype ι] (t : ℂ) (b : ι → ℂ) {z : ι → ℂ} (hz : ∀ (i : ι), z i ∈ Complex.slitPlane) : HasDerivAt (fun (s : ℂ) => regR s b z) (regL t b z) t

The exponent derivative of R exists and equals L for all complex parameters and slit nodes.