Iterates Source Radius

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_source_max_square {x : ℝ} (hx : 0 ≤ x) : max 1 x ^ 2 = max 1 (x ^ 2)

The square of the source maximum retains its exact two regimes.

theorem AVenhance.Infra.Section4.iterate_source_radius_identity {e γ R C₀ : ℝ} (he : 0 < e) (_hR : 0 < R) (hC₀ : 0 ≤ C₀) : C₀ * max 1 (e ^ (1 + γ / 2) / R) = e ^ (1 + γ / 2) * max (C₀ * e ^ (-1 - γ / 2)) (C₀ / R)

The printed source radius and F are exactly reciprocal diffusive scales.

theorem AVenhance.Infra.Section4.iterate_source_amplitude_parameter {e γ R C₀ ρ : ℝ} (he : 0 < e) (hR : 0 < R) : C₀ * (ρ * (C₀ * max 1 (e ^ (1 + γ / 2) / R)) ^ 2) = C₀ ^ 3 * ρ * max 1 (e ^ (2 + γ) * R ^ (-2))

The induction parameter is the printed C0-cubed smallness parameter.