Integral Antiderivative

LemmaCauchy rectangles#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1777. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as cauchy_for_rectangles.

Sources
Leancauchy_for_rectangles
Used by 1
Used byHorizontal strip

DefinitionIntegral along the taxicab path#

The blueprint of Strong PNT (Math Inc) states this definition at PNT/PNT1_ComplexAnalysis.tex, line 1810. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as If_taxicab.

Sources
LeanIf_taxicab
Used by 3
Used byIntegral form · Integral form · Integral form

LemmaIntegral form#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1819. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as def_If_z_plus_h.

Sources
Leandef_If_z_plus_h
Uses 1 · Used by 1
Proof usesIntegral along the taxicab path
Used byDifference form

LemmaIntegral form#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1830. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as def_If_z.

Sources
Leandef_If_z
Uses 1 · Used by 1
Proof usesIntegral along the taxicab path
Used byInitial form

LemmaIntegral form#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1841. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as def_If_w.

Sources
Leandef_If_w
Uses 1 · Used by 2
Proof usesIntegral along the taxicab path
Used byInitial form · Difference form

LemmaDifference form#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1853. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as diff_If_zh_w.

Sources
Leandiff_If_zh_w
Uses 2 · Used by 1
Proof usesIntegral form · Integral form
Used byL path

LemmaInitial form#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1866. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as diff_If_w_z_initial_form.

Sources
Leandiff_If_w_z_initial_form
Uses 2 · Used by 1
Proof usesIntegral form · Integral form
Used byShift integral

LemmaHorizontal strip#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1878. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as cauchy_for_horizontal_strip.

Sources
Leancauchy_for_horizontal_strip
Uses 1 · Used by 1
Proof usesCauchy rectangles
Used byRearrangement step

LemmaRearrangement step#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1890. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as cauchy_rearrangement_step1.

Sources
Leancauchy_rearrangement_step1
Uses 1 · Used by 1
Proof usesHorizontal strip
Used byShift integral

LemmaShift integral#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1909. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as diff_If_w_z.

Sources
Leandiff_If_w_z
Uses 2 · Used by 1
Proof usesRearrangement step · Initial form
Used byL path

LemmaL path#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1931. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as If_difference_is_L_path_integral.

Sources
LeanIf_difference_is_L_path_integral
Uses 2 · Used by 1
Proof usesShift integral · Difference form
Used byAdd-sub step

LemmaAdd-sub step#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1943. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as If_diff_add_sub_identity.

Sources
LeanIf_diff_add_sub_identity
Uses 1 · Used by 1
Proof usesL path
Used byLinearity split

LemmaLinearity split#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1955. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as If_diff_linearity.

Sources
LeanIf_diff_linearity
Uses 1 · Used by 1
Proof usesAdd-sub step
Used byDifference decomposition

LemmaIntegral of constant over L-path#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1981. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as integral_of_constant_over_L_path.

Sources
Leanintegral_of_constant_over_L_path
Used by 1
Used byDifference decomposition

LemmaDifference decomposition#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 1996. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as If_diff_decomposition_final.

Sources
LeanIf_diff_decomposition_final
Uses 2 · Used by 2
Proof usesLinearity split · Integral of constant over L-path
Used byBound on error term · Differentiability of \(I_f(z)\)

LemmaBound on error term#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 2025. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as bound_on_Err.

Sources
Leanbound_on_Err
Uses 1 · Used by 2
Proof usesDifference decomposition
Used byBound on error term ratio · Limit of \(S(z,h)\) is zero

LemmaBound on error term ratio#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 2056. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as bound_on_Err_ratio.

Sources
Leanbound_on_Err_ratio
Uses 1 · Used by 1
Proof usesBound on error term
Used byLimit of error term ratio is zero

LemmaLimit of \(S(z,h)\) is zero#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 2080. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as limit_of_S_is_zero.

Sources
Leanlimit_of_S_is_zero
Uses 1 · Used by 1
Proof usesBound on error term
Used byLimit of error term ratio is zero

LemmaLimit of error term ratio is zero#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 2116. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as limit_of_Err_ratio_is_zero.

Sources
Leanlimit_of_Err_ratio_is_zero
Uses 2 · Used by 1
Proof usesBound on error term ratio · Limit of \(S(z,h)\) is zero
Used byDifferentiability of \(I_f(z)\)

LemmaDifferentiability of \(I_f(z)\)#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 2140. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as If_is_differentiable_on.

Sources
LeanIf_is_differentiable_on
Uses 2 · Used by 1
Proof usesDifference decomposition · Limit of error term ratio is zero
Used byAntiderivative of logarithmic derivative

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.