ExitTimeCutoffLimitTail

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

Continuous representatives of the exit-time solutions, and the truncated family

The exit-time datum problem -∇·a∇u = 1 on y + □_n with zero boundary values is posed here for three coefficient fields: the truncated fields a_L = ν I + k_L at every truncation scale, the full stream field a = ν I + k, and the constant comparator σ_n I. All three have the same structure — a positive scalar symmetric part and a continuous skew part of arbitrary size — and that structure alone gives every solution a representative continuous on the open cube, by freezing the skew part at each interior point and applying the small-contrast interior estimate on a small ball. No smallness, no event and no bound on the solution is used.

The last section collects the truncated solutions with their representatives into one family indexed by the truncation scales, in the form the passage L → ∞ consumes.

Main results

• exists_isCubeRepresentative_of_isDirichletSolutionAt — a continuous representative for a coefficient field with scalar symmetric part and continuous skew part.
• exists_isCubeRepresentative_cutoff, exists_isCubeRepresentative_streamCoefficient, exists_isCubeRepresentative_comparator — the three instances.
• exists_cutoffSolutionFamily_linearAxisDatum — the truncated solutions with their representatives at every truncation scale.

References

• ABK26, the localized exit-time problem of Section 5.2, and the passage L → ∞ from the truncated fields a_L to a.

1. Continuous representatives from the structure of the coefficient

theorem Algsuperdiff.Section5.Provider.exists_isCubeRepresentative_of_isDirichletSolutionAt {d : ℕ} [NeZero d] (hd : 2 ≤ d) {nu : ℝ} (hnu : 0 < nu) {a : HCPolySupport.CoeffField d} {y : HCPolySupport.Vec d} {n : ℤ} (hsymm : ∀ (z : HCPolySupport.Vec d), HCPolySupport.symmPart (a z) = nu • 1) (hcont : ContinuousOn (fun (z : HCPolySupport.Vec d) => a z - nu • 1) (Support.cubeSetAt y n)) {i : Fin d} {u : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : Support.IsDirichletSolutionAt a y n u (Support.linearAxisDatum i)) : ∃ (uRep : HCPolySupport.Vec d → ℝ), Support.IsCubeRepresentative y n u uRep

The exit-time solution has a continuous representative. For a coefficient field whose symmetric part is the scalar field ν I with ν > 0 and whose skew part is continuous on the cube — of arbitrary size — the solution of the exit-time datum problem has a representative continuous on the open cube. The datum of the equation is the constant one, which is bounded, and that is the only bound the interior estimate consumes: nothing is assumed about the size of the solution.

theorem Algsuperdiff.Section5.Provider.exists_isCubeRepresentative_cutoff {d : ℕ} (M : Section3.ABKModel d) (L n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) {i : Fin d} {u : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField y n u (Support.linearAxisDatum i)) : ∃ (uRep : HCPolySupport.Vec d → ℝ), Support.IsCubeRepresentative y n u uRep

The truncated field's exit-time solution has a continuous representative, at every truncation scale. The symmetric part of a_L is ν I and the skew part k_L is continuous.

theorem Algsuperdiff.Section5.Provider.exists_isCubeRepresentative_streamCoefficient {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (omega : Field.FullSample d M.gamma) {i : Fin d} {u : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : Support.IsDirichletSolutionAt (Field.streamCoefficient M.nu omega) y n u (Support.linearAxisDatum i)) : ∃ (uRep : HCPolySupport.Vec d → ℝ), Support.IsCubeRepresentative y n u uRep

The full stream field's exit-time solution has a continuous representative. The symmetric part of a = ν I + k is ν I and the stream field k is continuous.

theorem Algsuperdiff.Section5.Provider.exists_isCubeRepresentative_comparator {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) {i : Fin d} {u : HCPolySupport.H1Function (Support.cubeSetAt y n)} (hu : Support.IsDirichletSolutionAt (fun (x : HCPolySupport.Vec d) => ↑(Section3.Annealed.sigmaBar M n) • 1) y n u (Support.linearAxisDatum i)) : ∃ (uRep : HCPolySupport.Vec d → ℝ), Support.IsCubeRepresentative y n u uRep

The comparator's exit-time solution has a continuous representative. The constant field σ_n I is its own symmetric part and its skew part vanishes.

2. The truncated family at every scale

theorem Algsuperdiff.Section5.Provider.exists_cutoffSolutionFamily_linearAxisDatum {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (i : Fin d) : ∃ (u : ℤ → HCPolySupport.H1Function (Support.cubeSetAt y n)) (uRep : ℤ → HCPolySupport.Vec d → ℝ), (∀ (L : ℤ), Support.IsDirichletSolutionAt (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField y n (u L) (Support.linearAxisDatum i)) ∧ ∀ (L : ℤ), Support.IsCubeRepresentative y n (u L) (uRep L)

The truncated exit-time solutions and their representatives, at every truncation scale. Solvability is unconditional for the rough field, and the representative comes from the structure of a_L; neither depends on the sample, on an event, or on the relative position of the truncation scale and the cube scale.