RootClauseBWellPlacedEndpoint

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

1. The obligation shape

theorem Algsuperdiff.Section4.Provider.Regularity.exists_rootDisplayClauseABoundaryC1Ae_wellPlaced (d : ℕ) [NeZero d] (hd : d ≠ 0) (cstar Crg : ℝ) (hcstar : 0 < cstar) (hCrg : 0 < Crg) : ∃ (Cfl : ℝ) (Citer : ℝ) (k : ℕ), 1 ≤ Cfl ∧ 11 ≤ k ∧ ∀ (Cedos : ℝ), Cfl ≤ Cedos → ∃ (Cest : ℝ) (gamma0 : ℝ), 0 ≤ Cest ∧ 0 < gamma0 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - Crg * √M.gamma → RootDisplayClauseABoundaryC1Ae M (stepOneC1 d Cedos 1 Citer k) Cest alpha

2. The endpoint, with no named conditional

theorem Algsuperdiff.Section4.Provider.Regularity.anomalous_regularity_provider_wellPlaced (d : ℕ) [NeZero d] (hd : d ≠ 0) (cstar Crg : ℝ) (hcstar : 0 < cstar) (hCrg : 0 < Crg) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ), ∃ (X : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable X ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad y‖ ≤ Real.rpow 3 (↑m / 2) * Kh) → Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ∀ n ≤ m, X omega ≤ ↑(m - n).toNat → ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * (↑m - ↑n))) * (ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg) + ENNReal.ofReal (√↑(Section3.Annealed.sigmaBar M m) * Real.rpow 3 (↑m / 2) * Kh)) ∧ (x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (C * Real.rpow 3 ((1 - alpha) * (↑m - ↑n))) * (ENNReal.ofReal √M.nu * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (u.grad y))) 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Kg)))