Formalpedia

The same actual rational Picard designation chosen from the original integral representation is geometrically connected over Q, and its underlying scheme is connected. Both complete original declarations are preserved, using the same integral representation witness and no replacement model. The named downstream consumer is flatness and surjectivity of the actual Picard norm-nineteen factors.

Let a scheme over a commutative ring carry an internal group object structure in the over category. The relative group-law multiplication-by-n scheme morphism is the underlying scheme morphism of the nth pointwise power of its identity morphism. This retains the original complete universes and arbitrary commutative base ring. The named downstream consumer is converting the actual Picard norm composites into multiplication by nineteen.

Let X be a nonempty preconnected scheme and let g be a finite etale endomorphism of X. Then g is surjective. The named downstream consumer is surjectivity of the actual rational Picard norm factors.

Let $k\ge1$, $s\in[0,1]$, and let $E_0\le E_1$ be the two smallest eigenvalues, counted with multiplicity, of the real symmetric path matrix with top-left entry $s-1$, adjacent off-diagonal entries $-s$, and all other entries zero. Then (...) If $s\le(k+1)/(2k+3)$, also $E_0\le-2s$ and $E_1\ge-2s\cos(\pi/(k+1))$.

For $s>0$ and $\pi/(k+1)<\theta<2\pi/(k+1)$, the following test locates the first excited eigenvalue: (...) These localization statements separate the finite path's spectral calculation from quantitative estimates on its gap.

Let K be a perfect characteristic-zero field and choose a two-affine cover of the actual curve over K. For K-valued points a,b of the same original rational represented Picard family, viewed in the over category,

(...)

The map is the original arithmetic class from a full degree-zero divisor presentation of the actual geometric line bundle. The result gives the faithful point comparison needed to detect the diamond and nineteen-norm scheme identities. The field and affine-cover parameters are explicit in the public statement; the complete original theorem type is preserved.

Let P be the same actual rational represented Picard scheme and let delta be its existing scheme diamond. Retain the original endomorphisms pi=3 id+2 delta and pi-bar=5 id-2 delta, using the commutative group law on the group of scheme morphisms to P. Both complete original constructor values and their full types, and the original group-object provider on P, are compared. The named downstream consumer is the proof that both composites equal multiplication by nineteen. The constructor package does not assert isogeny degrees or rational rank.

The volume of the nonnegative unit simplex in dimension k+1 equals its dimension-k volume divided by k+1.

At cutoff zero, the identity holds in every dimension: for k > 0 the set is the singleton zero vector and has zero volume; for k = 0 both sides equal 1. This isolates the singular scale that the invertible linear-map change-of-variables argument cannot handle. The proof route is to characterize the cutoff-zero set, use nullity of a singleton in positive-dimensional Euclidean space, and simplify separately in dimension zero.

For a strictly positive cutoff U, scaling every coordinate of the unit simplex by U multiplies its volume by U raised to the dimension. This removes the nondegenerate change-of-variables argument from the parent; prove it using the pinned Mathlib linear-map volume scaling theorem, the determinant of scalar multiplication, and the image of the unit simplex. The remaining core obligation is this positive-scale change-of-variables calculation.

Retain the existing generic-compatible rational diamond as an actual endomorphism of the same represented Picard scheme. For every perfect characteristic-zero field K and a two-affine cover of the literal curve over K, retain the original group homomorphism from its K-valued Picard points to the multiplicative form of the actual arithmetic Pic0 group. The original Poincare unit facts supply the identity constructor law. Both complete constructor values, both original unit-fact types, both scalar algebra providers and the original Picard group-object provider are compared. The named downstream consumer is the geometric cyclotomic and genuine nineteen-norm scheme identity. The two already accepted kernel and multiplication proofs needed by these constructor laws are retained with explicit local instance names. This is a constructor export of existing checked mathematics, with no additional owned theorem acceptance credit.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.essentiallySelfAdjointOn_finiteModes_of_core_bounds_comm_inc (c : ι → ℝ) (hc : ∀ k, 0 ≤ c k) (H₀ : lpFiniteModes ι →ₗ[ℂ] L2I ι) (A : ℝ) (hsym : ∀ u v : lpFiniteModes ι, (inner ℂ (H₀ u) ((v : L2I ι)) : ℂ) = inner ℂ ((u : L2I ι)) (H₀ v)) (hA : CoreRelBound c H₀ A) (hcomm : ∀ u : lpFiniteModes ι, (inner ℂ (H₀ u) ((diagMax c (inclC c u) : L2I ι)) : ℂ).im = 0) : EssentiallySelfAdjointOn (lpFiniteModes ι) H₀

Formalization note: Lean 4 identifier BookProof.CoreBounds.essentiallySelfAdjointOn_finiteModes_of_core_bounds_comm_inc.

Replaces the unuploadable node BookProof_CoreBounds_essentiallySelfAdjointOn_finiteModes_of_core_bounds_comm, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.essentiallySelfAdjointOn_finiteModes_of_core_bounds_inc (c : ι → ℝ) (hc : ∀ k, 0 ≤ c k) (H₀ : lpFiniteModes ι →ₗ[ℂ] L2I ι) (A B : ℝ) (hB : 0 ≤ B) (hsym : ∀ u v : lpFiniteModes ι, (inner ℂ (H₀ u) ((v : L2I ι)) : ℂ) = inner ℂ ((u : L2I ι)) (H₀ v)) (hA : CoreRelBound c H₀ A) (hcomm : ∀ u : lpFiniteModes ι, |(-2 : ℝ) * (inner ℂ (H₀ u) ((diagMax c (inclC c u) : L2I ι)) : ℂ).im| ≤ B * (inner ℂ ((u : L2I ι)) ((diagMax c (inclC c u) : L2I ι)) : ℂ).re) : EssentiallySelfAdjointOn (lpFiniteModes ι) H₀

Formalization note: Lean 4 identifier BookProof.CoreBounds.essentiallySelfAdjointOn_finiteModes_of_core_bounds_inc.

Replaces the unuploadable node BookProof_CoreBounds_essentiallySelfAdjointOn_finiteModes_of_core_bounds, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.coreExt_symmetricOn_inc [DecidableEq ι] {c : ι → ℝ} {H₀ : lpFiniteModes ι →ₗ[ℂ] L2I ι} {A : ℝ} (hA : CoreRelBound c H₀ A) (hsym : ∀ u v : lpFiniteModes ι, (inner ℂ (H₀ u) ((v : L2I ι)) : ℂ) = inner ℂ ((u : L2I ι)) (H₀ v)) : SymmetricOn (maxDom c) (coreExt hA)

Formalization note: Lean 4 identifier BookProof.CoreBounds.coreExt_symmetricOn_inc.

Replaces the unuploadable node BookProof_CoreBounds_coreExt_symmetricOn, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.coreExt_commForm_le_inc [DecidableEq ι] {c : ι → ℝ} {H₀ : lpFiniteModes ι →ₗ[ℂ] L2I ι} {A B : ℝ} (hA : CoreRelBound c H₀ A) (hcomm : ∀ u : lpFiniteModes ι, |(-2 : ℝ) * (inner ℂ (H₀ u) ((diagMax c (inclC c u) : L2I ι)) : ℂ).im| ≤ B * (inner ℂ ((u : L2I ι)) ((diagMax c (inclC c u) : L2I ι)) : ℂ).re) (x : maxDom c) : |commForm (coreExt hA) (diagMax c) x| ≤ B * quadForm (diagMax c) x

Formalization note: Lean 4 identifier BookProof.CoreBounds.coreExt_commForm_le_inc.

Replaces the unuploadable node BookProof_CoreBounds_coreExt_commForm_le, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.tendsto_trunc_inc [DecidableEq ι] (c : ι → ℝ) (x : maxDom c) : Tendsto (fun S : Finset ι => ((trunc c x S : lpFiniteModes ι) : L2I ι)) atTop (𝓝 ((x : L2I ι)))

Formalization note: Lean 4 identifier BookProof.CoreBounds.tendsto_trunc_inc.

Replaces the unuploadable node BookProof_CoreBounds_tendsto_trunc, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.coreExt_core_inc [DecidableEq ι] {c : ι → ℝ} {H₀ : lpFiniteModes ι →ₗ[ℂ] L2I ι} {A : ℝ} (hA : CoreRelBound c H₀ A) (u : lpFiniteModes ι) : coreExtFun c H₀ (inclC c u) = H₀ u

Formalization note: Lean 4 identifier BookProof.CoreBounds.coreExt_core_inc.

Replaces the unuploadable node BookProof_CoreBounds_coreExt_core, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterCoreBoundsEsa.

BookProof.CoreBounds.norm_coreExt_le_inc [DecidableEq ι] {c : ι → ℝ} {H₀ : lpFiniteModes ι →ₗ[ℂ] L2I ι} {A : ℝ} (hA : CoreRelBound c H₀ A) (x : maxDom c) : ‖coreExt hA x‖ ≤ A * ‖(diagMax c x : L2I ι)‖

Formalization note: Lean 4 identifier BookProof.CoreBounds.norm_coreExt_le_inc.

Replaces the unuploadable node BookProof_CoreBounds_norm_coreExt_le, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterAbelianClassificationList.

BookProof.ChapterAbelianClassificationList.abelian_summand_standard_model_inc : (IsHilbertSum ℂ (fun b : Bool => Lp ℂ 2 (mu.restrict (splitSet (atomSet mu) b))) (splitEmbed (measurableSet_atomSet mu))) ∧ (∀ (b : Bool) (g : ℝ → ℂ) (hg : MemLp g ⊤ mu) (u : Lp ℂ 2 (mu.restrict (splitSet (atomSet mu) b))), splitEmbed (measurableSet_atomSet mu) b (multOp g (hg.restrict _) u) = multOp g hg (splitEmbed (measurableSet_atomSet mu) b u)) ∧ (∃ B : HilbertBasis (atomSet (mu.restrict (atomSet mu))) ℂ (Lp ℂ 2 (mu.restrict (atomSet mu))), ∀ (g : ℝ → ℂ) (hg : MemLp g ⊤ (mu.restrict (atomSet mu))) (a : atomSet (mu.restrict (atomSet mu))), multOp g hg (B a) = g (a : ℝ) • B a) ∧ (mu (atomSet mu)ᶜ ≠ 0 → ∃ U : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1)) ≃ₗᵢ[ℂ] Lp ℂ 2 (mu.restrict (atomSet mu)ᶜ), ∀ (g : ℝ → ℂ) (hg : MemLp g ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1))) (u : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))), (U (multOp g hg u) : ℝ → ℂ) =ᵐ[mu.restrict (atomSet mu)ᶜ] fun x => g (cdf (normalized (mu.restrict (atomSet mu)ᶜ)) x) * (U u : ℝ → ℂ) x)

Formalization note: Lean 4 identifier BookProof.ChapterAbelianClassificationList.abelian_summand_standard_model_inc.

Replaces the unuploadable node BookProof_ChapterAbelianClassificationList_abelian_summand_standard_model, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterAbelianClassificationList.

BookProof.ChapterAbelianClassificationList.diffuse_finite_multiplication_model_inc (hne : nu Set.univ ≠ 0) : ∃ U : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1)) ≃ₗᵢ[ℂ] Lp ℂ 2 nu, ∀ (g : ℝ → ℂ) (hg : MemLp g ⊤ (volume.restrict (Set.Icc (0 : ℝ) 1))) (u : Lp ℂ 2 (volume.restrict (Set.Icc (0 : ℝ) 1))), (U (multOp g hg u) : ℝ → ℂ) =ᵐ[nu] fun x => g (cdf (normalized nu) x) * (U u : ℝ → ℂ) x

Formalization note: Lean 4 identifier BookProof.ChapterAbelianClassificationList.diffuse_finite_multiplication_model_inc.

Replaces the unuploadable node BookProof_ChapterAbelianClassificationList_diffuse_finite_multiplication_model, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.

Prove the following Lean 4 theorem from ChapterAbelianClassificationList.

BookProof.ChapterAbelianClassificationList.isProbabilityMeasure_normalized_inc (hne : nu Set.univ ≠ 0) : IsProbabilityMeasure (normalized nu)

Formalization note: Lean 4 identifier BookProof.ChapterAbelianClassificationList.isProbabilityMeasure_normalized_inc.

Replaces the unuploadable node BookProof_ChapterAbelianClassificationList_isProbabilityMeasure_normalized, whose statement name is already declared inside its published definition bundle; the _inc suffix publishes the same statement as its own node.