MATHLIBANNEX / PROJECT LFH

Zero weak gradients and constancy

Back to Project mathematical routes

Scope

The weak equation makes local mollifications constant, giving local almost-everywhere constancy of the original function. Overlap and countable gluing arguments give global almost-everywhere constancy on an open preconnected domain. The separate continuous case upgrades this to pointwise constancy.

10 direct Cards + 0 reused prerequisites = 10 unique Cards. This count is a selected Card closure, not a source-declaration count.

Route reading PDF · Preserved source exploration

Cards in this route

Read this route with prerequisites

Reference index: direct Cards and reused prerequisites

Direct references: SR099 — Divergence as the trace of a derivative · SR120 — Vanishing weak gradient tested by divergence · SR444 — Gluing one almost-everywhere constant over a countable cover · SR449 — Identifying constants on an open overlap · SR452 — From local to global almost-everywhere constancy · SR155 — Differentiating a local mollification through its kernel · SR157 — Zero weak gradient gives zero derivatives of local mollifications · SR117 — Local almost-everywhere constancy from the weak equation · SR118 — Global almost-everywhere constancy on a preconnected domain · SR119 — A continuous function with zero weak gradient is constant

Reused prerequisites: None in this scope.

Dependency-first reading route

Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.

10 Cards

Level 0 (4 Cards)

Level 1 (2 Cards)

Level 2 (1 Card)

Level 2

Zero weak gradient gives zero derivatives of local mollifications

Substitutes a translated smooth kernel into the weak equation and tracks the reflection sign.

MathlibAnnex.WeakGradient.localMollification_fderiv_apply_eq_zero

Immediate Card prerequisites: Vanishing weak gradient tested by divergence · Differentiating a local mollification through its kernel

Used by in this scope: Local almost-everywhere constancy from the weak equation

Open Declaration Card Read exact source

Level 3 (1 Card)

Level 4 (1 Card)

Level 5 (1 Card)