HomSeamComposition

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The generator-renormalization conclusion

GeneratorRenormalizationShape d cstar names the frozen conclusion: the effective coefficient approximation, moments of the random error envelope, and the almost-everywhere comparison estimates for Dirichlet solutions.

This module defines that conclusion. The composition with a model-dependent clause constant is proved in HomSeamCompositionCcg, and the theorem generator_renormalization_provider_final in HomSeamProviderFinal constructs the shape for every dimension and positive cstar from the model assumptions. The clause and energy supply interfaces used by that route are recorded in HomSeamSupClauseCcgFree; the downstream seam data carry the clause constant as an explicit parameter or existential witness.

1. The frozen conclusion, named

def Algsuperdiff.Section4.Provider.Homogenization.GeneratorRenormalizationShape (d : ℕ) (cstar : ℝ) : Prop

THE FROZEN generator_renormalization CONCLUSION.

Byte-transcribed from the FROZEN-STATEMENT block of Algsuperdiff/Frozen/Section4/GeneratorRenormalization.lean (which is NOT imported), modulo this file's opens.

Equations

• One or more equations did not get rendered due to their size.