wamlart

Solved 50

• Theorem 10.20 — $d(d\omega) = 0$Proved

  Sep 2026

• Theorem 10.25 — integration and pullbackProved

  Sep 2026

• Theorem 10.9 — change of variablesProved

  Sep 2026

• Theorems 8.11-8.12 — best mean-square approximation and Bessel's inequalityDisproved

  Sep 2026

• Theorem 9.28 — implicit function theoremProved

  Sep 2026

• Theorem 8.5 — identity theorem for power seriesProved

  Sep 2026

• The Lean 4 theorem `nsQuadraticDiffH_hashimoto_selects` in the `ChapterNavierStokesDiffHashimoto` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsDiffH_hashimoto_selects` in the `ChapterNavierStokesDiffHashimoto` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsDiffH_selfAdjoint_extension` in the `ChapterNavierStokesDiffHashimoto` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsDiffH_selfAdjoint_extension_unique` in the `ChapterNavierStokesDiffHashimoto` chapter of the timepiece formalizationProved

  Sep 2026

• Theorem 8.15 — uniform approximation by trigonometric polynomialsProved

  Sep 2026

• Theorem 7.32 — Stone–WeierstrassDisproved

  Sep 2026

• Theorems 7.24-7.25 — Arzelà–AscoliProved

  Sep 2026

• Theorem 7.26 — Weierstrass approximation theoremProved

  Sep 2026

• Theorem 8.3 — interchanging the order of summationProved

  Sep 2026

• Theorem 11.45 — Parseval's identity for a complete orthonormal systemProved

  Sep 2026

• Theorem 11.42 — the Riesz–Fischer theoremProved

  Sep 2026

• Theorem 11.38 — continuous functions are dense in $\mathscr{L}^2[a,b]$Proved

  Sep 2026

• Theorem 11.35 — the Schwarz inequality in $\mathscr{L}^2$Proved

  Sep 2026

• Theorem 11.32 — Lebesgue's dominated convergence theoremProved

  Sep 2026

• Theorem 11.31 — Fatou's theoremProved

  Sep 2026

• Theorem 11.30 — term-by-term integration of a series of nonnegative functionsProved

  Sep 2026

• Theorem 11.28 — Lebesgue's monotone convergence theoremProved

  Sep 2026

• Theorems 11.26 and 11.27 — comparison and the triangle inequalityProved

  Sep 2026

• Theorem 11.24 — the integral is a countably additive set functionProved

  Sep 2026

• Theorem 11.17 — suprema and upper limits of measurable functionsProved

  Sep 2026

• Theorems 11.16 and 11.18 — algebraic operations on measurable functionsProved

  Sep 2026

• Theorem 7.11 — interchanging two limitsProved

  Sep 2026

• Theorem 5.12 — derivatives have the intermediate value propertyProved

  Sep 2026

• Theorem 5.13 — L'Hospital's rule, the $0/0$ caseProved

  Sep 2026

• Theorem 7.12 — uniform limits of continuous functionsProved

  Sep 2026

• Theorem 9.24 — inverse function theoremProved

  Sep 2026

• Theorem 10.8 — partitions of unityProved

  Sep 2026

• Theorem 9.19 — mean value inequality on a convex setProved

  Sep 2026

• Theorem 9.23 — the contraction principleProved

  Sep 2026

• Theorem 8.6 — properties of the exponential functionProved

  Sep 2026

• Theorem 8.7 — the trigonometric functions and $\pi$Proved

  Sep 2026

• Theorem 8.8 — the fundamental theorem of algebraProved

  Sep 2026

• Theorem 8.18 — functional equation and log-convexity of $\Gamma$Proved

  Sep 2026

• Theorem 8.19 — Bohr–Mollerup characterization of $\Gamma$Proved

  Sep 2026

• The Lean 4 theorem `harmonic_add_subquadratic_stone_flow` in the `ChapterHermiteQuadraticEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `harmonicCore_stone_flow` in the `ChapterQgHermiteOscillatorEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sectorGround_ge_temple` in the `ChapterSirkCertifiedGap` chapter of the timepiece formalizationProved

  Sep 2026

• (hnu : 0 < nu) (f : Fin 3 → ℝ) : ∃ (T : UnboundedSelfAdjoint (L2I Vel)) (U : ℝ → (L2I Vel →L[ℂ] L2I Vel)), IsSelfAdjointExtension (lagrangianCore (lagCanData nu hnu f)) T.op ∧...Proved

  Sep 2026

• (kappa : Fin D → ℝ) (v : R → Fin D → ℝ) (p : MvPolynomial (Fin D) ℂ) : sqSumPoly kappa v p = kinPart kappa p + potPoly v * pProved

  Sep 2026

• {kappa : Fin D → ℝ} {v : R → Fin D → ℝ} {km B : ℝ} (hkm : 0 ≤ km) (hk : ∀ j, |kappa j| ≤ km) (hB0 : 0 ≤ B) (hB : ∀ x : Vd D, potFun v x ≤ B * ‖x‖ ^ 2) (p :...Proved

  Sep 2026

• {v : R → Fin D → ℝ} {B : ℝ} (hB0 : 0 ≤ B) (hB : ∀ x : Vd D, potFun v x ≤ B * ‖x‖ ^ 2) (p : MvPolynomial (Fin D) ℂ) : ‖pgLp (potPoly v * p)‖ ≤ 4 * B * ‖pgLp (harmPoly *...Proved

  Sep 2026

• (kappa : Fin D → ℝ) (v : R → Fin D → ℝ) (p : MvPolynomial (Fin D) ℂ) : commPoly kappa v p = ((commConst kappa v : ℝ) : ℂ) • p + (∑ j : Fin D, ((-(kappa j) / 2 : ℝ) : ℂ)...Proved

  Sep 2026

• (q w : MvPolynomial (Fin D) ℂ) : |(gaussInt (cpoly q * w)).im| ≤ ‖pgLp q‖ * ‖pgLp w‖Proved

  Sep 2026

• The Lean 4 theorem `nsDiffH_shiftInvert_selects` in the `ChapterNavierStokesDiffHashimoto` chapter of the timepiece formalizationProved

  Sep 2026

Posted 50

• A finite sum bounded by a product of truncated termsProved

  Sep 2026

• Exact reciprocal sum from a bilinear recurrenceProved

  Sep 2026

• A second-order reciprocal average stays between one and twoProved

  Sep 2026

• Continuous iteration above the identity diverges to infinityProved

  Sep 2026

• The scaled limit of an index-dependent square-root recurrenceProved

  Sep 2026

• A fourth-order recurrence grows slower than the square of its indexProved

  Sep 2026

• A positive square-root iteration must be constantProved

  Sep 2026

• An invariant interval for a rational recurrenceProved

  Sep 2026

• Boundedness of a square-root averaging recurrenceProved

  Sep 2026

• Integer terms from a consecutive-product square invariantProved

  Sep 2026

• Convergence from bounds between consecutive termsProved

  Sep 2026

• Failure of uniform convergence for a growing narrow spikeProved

  Sep 2026

• Consecutive-term ratio bounds for a quadratic recurrenceProved

  Sep 2026

• A sequence characterized by its partial sums of cubesProved

  Sep 2026

• Vanishing scaled terms of an index-dependent rational recurrenceProved

  Sep 2026

• Limit of a recurrence with squared reciprocal weightsProved

  Sep 2026

• Integrality of a square-root recurrence via a Pell invariantProved

  Sep 2026

• Limit of a quadratic iteration with a rational error boundProved

  Sep 2026

• Closed form of a second-order linear recurrenceProved

  Sep 2026

• Convergence under a preceding-sum boundProved

  Sep 2026

• Largest-term bound from two finite-sequence momentsProved

  Sep 2026

• Bounds, strict increase, and limit of a logistic recurrenceProved

  Sep 2026

• Exact limit of a quadratic-over-linear recurrenceProved

  Sep 2026

• Convergence of a quadratic square-root approximationProved

  Sep 2026

• Exact limit of reciprocal iterationProved

  Sep 2026

• Exact limit of a second-order averaging recurrenceProved

  Sep 2026

• Accuracy after thirty Newton iterations for the square root of 2002Proved

  Sep 2026

• Divergence to positive infinity for a reciprocal-increment recurrenceProved

  Sep 2026

• An invariant interval for a quartic rational recurrenceProved

  Sep 2026

• A strict partial-sum bound for a rational multiplier recurrenceProved

  Sep 2026

• A strict rational lower bound for a quadratic recurrenceProved

  Sep 2026

• Boundedness from a quadratic inequality between adjacent sequence termsProved

  Sep 2026

• The floor of a telescoping sum along a quadratic recurrenceProved

  Sep 2026

• A harmonic lower bound for an implicit quadratic recurrenceProved

  Sep 2026

• Monotonicity of an iterated square-root sequenceProved

  Sep 2026

• A sum-of-squares upper bound from a reciprocal difference constraintProved

  Sep 2026

• Exact attained minimum of a sum of squares under a reciprocal constraintProved

  Sep 2026

• A sharp sum bound from reciprocal quadratic denominatorsProved

  Sep 2026

• A strict lower bound for the fractional part of a nonintegral cube rootProved

  Sep 2026

• A product bound from reciprocal weighted sumsProved

  Sep 2026

• A linear identity from two reciprocal quadratic constraintsProved

  Sep 2026

• Determining a sequence from a symmetric index relationProved

  Sep 2026

• A sum-of-squares bound from a quartic and product constraintProved

  Sep 2026

• A reciprocal lower bound from a quadratic denominator identityProved

  Sep 2026

• Bounds on a sum under a cube-root constraintProved

  Sep 2026

• Two solutions of a conjugate cube-root equationProved

  Sep 2026

• A sextic polynomial has no real rootsProved

  Sep 2026

• An inequality from a product of adjacent sumsProved

  Sep 2026

• Uniqueness of a solution to a real cube-root equationProved

  Sep 2026

• Classification of a functional equation involving complementary cubesProved

  Sep 2026