Documentation Verification Report

Sobolev

📁 Source: PrimeNumberTheoremAnd/Sobolev.lean

Statistics

Metric	Count
Definitions `CS`, `deriv`, `instCoeFunForallReal`, `instCoeRealComplex`, `instHSMulReal`, `instNeg`, `neg`, `scale`, `smul`, `toFun`, `W1`, `deriv`, `instCoeFunForallReal`, `instSub`, `of_Schwartz`, `sub`, `toFun`, `W21`, `instCoeCSOfNatNatComplex`, `instCoeSchwartzMapRealComplex`, `instHMulCSOfNatNatComplex`, `instHMulCSOfNatNatRealComplex`, `instNorm`, `norm`, `ofCS2`, `funscale`, `trunc`, `instCoeCSOfNatNatReal`, `instCoeFunForallReal`, `toCS`	30
Theorems `bounded`, `continuous`, `deriv_apply`, `deriv_scale`, `deriv_scale'`, `deriv_smul`, `ext`, `ext_iff`, `h1`, `h2`, `hasDerivAt`, `hasDerivAt_scale`, `neg_apply`, `smul_apply`, `tendsto_scale`, `continuous`, `differentiable`, `hasDerivAt`, `integrable`, `integrable_iteratedDeriv_Schwarz`, `iteratedDeriv_sub`, `smooth`, `hf`, `hf'`, `hf''`, `norm_nonneg`, `W21_approximation`, `contDiff_ofReal`, `tendsto_funscale`, `h3`, `h4`, `le_one`, `nonneg`, `zero`, `zero_at`	35
Total	65

CS

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	5 math math: `deriv_scale`, `deriv_scale'`, `deriv_smul`, `hasDerivAt`, `deriv_apply`
`instCoeFunForallReal` 📖	CompOp	—
`instCoeRealComplex` 📖	CompOp	—
`instHSMulReal` 📖	CompOp	3 math math: `deriv_scale`, `smul_apply`, `deriv_smul`
`instNeg` 📖	CompOp	1 math math: `neg_apply`
`neg` 📖	CompOp	—
`scale` 📖	CompOp	5 math math: `hasDerivAt_scale`, `deriv_scale`, `deriv_scale'`, `tendsto_scale`, `W21_approximation`
`smul` 📖	CompOp	—
`toFun` 📖	CompOp	27 math math: `bounded`, `integrable_norm_fourier_scaled_of_CS2`, `decay_bounds_cor_aux`, `limiting_cor`, `trunc.nonneg`, `trunc.le_one`, `hasDerivAt_scale`, `smul_apply`, `trunc.zero_at`, `deriv_scale'`, `trunc.h4`, `fourier_decay_of_CS2`, `ext_iff`, `h2`, `limiting_fourier_aux`, `limiting_fourier_lim3_gt_zero`, `continuous`, `tendsto_scale`, `hasDerivAt`, `trunc.zero`, `h1`, `trunc.h3`, `neg_apply`, `limiting_fourier_aux_gt_zero`, `limiting_fourier`, `limiting_fourier_lim3`, `deriv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bounded` 📖	mathematical	—	`toFun`	—	`continuous` `h2`
`continuous` 📖	mathematical	—	`toFun`	—	`h1`
`deriv_apply` 📖	mathematical	—	`toFun` `deriv`	—	—
`deriv_scale` 📖	mathematical	—	`deriv` `scale` `CS` `instHSMulReal`	—	`ext` `hasDerivAt`
`deriv_scale'` 📖	mathematical	—	`toFun` `deriv` `scale`	—	`deriv_scale` `smul_apply`
`deriv_smul` 📖	mathematical	—	`deriv` `CS` `instHSMulReal`	—	`ext` `hasDerivAt`
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`h1` 📖	mathematical	—	`toFun`	—	—
`h2` 📖	mathematical	—	`toFun`	—	—
`hasDerivAt` 📖	mathematical	—	`toFun` `deriv`	—	`h1`
`hasDerivAt_scale` 📖	mathematical	—	`toFun` `scale`	—	`deriv_scale'` `hasDerivAt`
`neg_apply` 📖	mathematical	—	`toFun` `CS` `instNeg`	—	—
`smul_apply` 📖	mathematical	—	`toFun` `CS` `instHSMulReal`	—	—
`tendsto_scale` 📖	mathematical	—	`toFun` `scale`	—	`tendsto_funscale` `continuous`

W1

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	1 math math: `hasDerivAt`
`instCoeFunForallReal` 📖	CompOp	—
`instSub` 📖	CompOp	1 math math: `W21_approximation`
`of_Schwartz` 📖	CompOp	—
`sub` 📖	CompOp	—
`toFun` 📖	CompOp	23 math math: `integrable`, `limiting_cor_W21`, `continuous`, `limiting_fourier_lim2`, `bound_I2`, `W21.hf''`, `summable_fourier`, `W21.hf`, `differentiable`, `fourierIntegral_self_add_deriv_deriv`, `bound_I1`, `limiting_fourier_lim2_gt_zero`, `bound_main`, `summable_fourier_aux`, `decay_bounds_key`, `continuous_FourierIntegral`, `W21.integrable_fourier`, `bound_I1'`, `W21.hf'`, `hasDerivAt`, `limiting_fourier_lim1`, `smooth`, `decay_bounds_cor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous` 📖	mathematical	—	`toFun`	—	`smooth`
`differentiable` 📖	mathematical	—	`toFun`	—	`smooth`
`hasDerivAt` 📖	mathematical	—	`toFun` `deriv`	—	`differentiable`
`integrable` 📖	mathematical	—	`toFun`	—	—
`integrable_iteratedDeriv_Schwarz` 📖	—	—	—	—	—
`iteratedDeriv_sub` 📖	—	—	—	—	—
`smooth` 📖	mathematical	—	`toFun`	—	—

W21

Definitions

Name	Category	Theorems
`instCoeCSOfNatNatComplex` 📖	CompOp	—
`instCoeSchwartzMapRealComplex` 📖	CompOp	—
`instHMulCSOfNatNatComplex` 📖	CompOp	—
`instHMulCSOfNatNatRealComplex` 📖	CompOp	1 math math: `W21_approximation`
`instNorm` 📖	CompOp	2 math math: `decay_bounds_key`, `W21_approximation`
`norm` 📖	CompOp	6 math math: `bound_I2`, `bound_I1`, `bound_main`, `summable_fourier_aux`, `norm_nonneg`, `bound_I1'`
`ofCS2` 📖	CompOp	1 math math: `W21_approximation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hf` 📖	mathematical	—	`W1.toFun`	—	`W1.integrable`
`hf'` 📖	mathematical	—	`W1.toFun`	—	`W1.integrable`
`hf''` 📖	mathematical	—	`W1.toFun`	—	`W1.integrable`
`norm_nonneg` 📖	mathematical	—	`norm`	—	—

(root)

Definitions

Name	Category	Theorems
`CS` 📖	CompData	5 math math: `CS.deriv_scale`, `CS.smul_apply`, `CS.deriv_smul`, `CS.neg_apply`, `W21_approximation`
`W1` 📖	CompData	—
`W21` 📖	CompOp	2 math math: `decay_bounds_key`, `W21_approximation`
`funscale` 📖	CompOp	1 math math: `tendsto_funscale`
`trunc` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`W21_approximation` 📖	mathematical	—	`W21` `W21.instNorm` `W1.instSub` `W21.ofCS2` `CS` `W21.instHMulCSOfNatNatRealComplex` `CS.scale` `trunc.toCS`	—	`CS.continuous` `CS.deriv_scale'` `CS.hasDerivAt_scale` `CS.hasDerivAt` `trunc.le_one` `trunc.nonneg` `trunc.zero` `W1.continuous` `W21.hf` `W1.hasDerivAt` `CS.bounded` `CS.deriv_scale` `CS.deriv_smul` `W21.hf'` `W21.hf''` `trunc.zero_at` `CS.tendsto_scale`
`contDiff_ofReal` 📖	—	—	—	—	—
`tendsto_funscale` 📖	mathematical	—	`funscale`	—	—

trunc

Definitions

Name	Category	Theorems
`instCoeCSOfNatNatReal` 📖	CompOp	—
`instCoeFunForallReal` 📖	CompOp	—
`toCS` 📖	CompOp	7 math math: `nonneg`, `le_one`, `zero_at`, `h4`, `zero`, `h3`, `W21_approximation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`h3` 📖	mathematical	—	`CS.toFun` `toCS`	—	—
`h4` 📖	mathematical	—	`CS.toFun` `toCS`	—	—
`le_one` 📖	mathematical	—	`CS.toFun` `toCS`	—	`h4`
`nonneg` 📖	mathematical	—	`CS.toFun` `toCS`	—	`h3`
`zero` 📖	mathematical	—	`CS.toFun` `toCS`	—	`le_one` `h3`
`zero_at` 📖	mathematical	—	`CS.toFun` `toCS`	—	`zero`

---

← Back to Index