SharpSimplexMean

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_abs_entry_increment_le_simplexMean_add_cubeOscGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n L : ℤ) (omega : Cutoff.ShellSeq d) (T : Whitney.KuhnCell d) (hTQ : T.openCarrier ⊆ HCPolySupport.openCubeSet Q) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet Q) (i l : Fin d) : |(Cutoff.finiteShellIncrement omega n L).toFun x i l| ≤ |simplexIncrementValue n L omega T i l| + √↑d * BadEvents.cubeOscGauge Q (Stream.shellIncrement omega n L)

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_w1Infinity_incrementUnitCube₂_le_simplexMean_add_cubeOscGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n L : ℤ) (omega : Cutoff.CutoffSample d) (T : Whitney.KuhnCell d) (hTQ : T.openCarrier ⊆ HCPolySupport.openCubeSet Q) : (BadEvents.incrementUnitCube₂ Q n L omega).w1Infinity ≤ BadEvents.cubeOscGauge Q (Stream.shellIncrement (↑omega) n L) + ↑d ^ 2 * (HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue n L (↑omega) T) + √↑d * BadEvents.cubeOscGauge Q (Stream.shellIncrement (↑omega) n L))

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSimplexW1Const (d : ℕ) : ℝ

The dimension-dependent Sobolev constant for the simplex probe.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeSimplexW1Const d = 1 + ↑d ^ 2 * (1 + √↑d)

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSimplexW1Const_nonneg (d : ℕ) : 0 ≤ probeSimplexW1Const d

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_w1Infinity_incrementUnitCube₂_sq_le_simplexMean_sq_add_cubeOscGauge_sq {d : ℕ} (Q : HCPolySupport.TriadicCube d) (n L : ℤ) (omega : Cutoff.CutoffSample d) (T : Whitney.KuhnCell d) (hTQ : T.openCarrier ⊆ HCPolySupport.openCubeSet Q) : (BadEvents.incrementUnitCube₂ Q n L omega).w1Infinity ^ 2 ≤ 2 * probeSimplexW1Const d ^ 2 * (HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue n L (↑omega) T) ^ 2 + BadEvents.cubeOscGauge Q (Stream.shellIncrement (↑omega) n L) ^ 2)

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_w1Infinity_incrementUnitCube₂_sq_le_simplexMean_sq_add_oscThreshold_sq {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {L : ℤ} (hL : Q.scale ≤ L) {omega : Cutoff.CutoffSample d} (homega : omega ∉ BadEvents.badOsc M Q) (T : Whitney.KuhnCell d) (hTQ : T.openCarrier ⊆ HCPolySupport.openCubeSet Q) : (BadEvents.incrementUnitCube₂ Q Q.scale L omega).w1Infinity ^ 2 ≤ 2 * probeSimplexW1Const d ^ 2 * (HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue Q.scale L (↑omega) T) ^ 2 + BadEvents.oscThreshold M Q.scale ^ 2)

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_inv_cstar_mul_gamma_mul_rpow_mul_oscThreshold_sq {d : ℕ} (M : ABKModel d) (j : ℤ) : (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑j)) * BadEvents.oscThreshold M j ^ 2 = BadEvents.deltaOsc d ^ 2

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSimplexMeanSensitivityConst (d : ℕ) : ℝ

The sensitivity constant for the mean simplex probe.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSimplexMeanSensitivityConst_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ probeSimplexMeanSensitivityConst d

Weighted layer bridge for the simplex means

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeLayerSimplexMeanSq {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (n1 n2 : ℤ) (omega : Cutoff.CutoffSample d) : ℝ

The weighted sum of squared simplex increment norms over a Whitney layer.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeLayerSimplexMeanSq_le_sqrt_mass_mul_sqrt_fourth {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (hstep : hn n ≤ hn (n + 1) + 1) (n1 n2 : ℤ) (omega : Cutoff.CutoffSample d) : probeLayerSimplexMeanSq m hn n n1 n2 omega ≤ √(∑ Q ∈ Whitney.whitneyLayer m hn n, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q) * √(layerSimplexFourthMass m hn n n1 n2 omega)

Refined collar carrier with the same simplex mean

The actual weighted good-cell layer

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeMeanGoodBaseConst (d : ℕ) : ℝ

The dimension-dependent constant for the good-layer base mean contribution.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeMeanGoodWaveConst {d : ℕ} (M : ABKModel d) : ℝ

The model-dependent constant for the good-layer wave mean contribution.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeMeanGoodBaseConst_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ probeMeanGoodBaseConst d

theorem Algsuperdiff.Section3.Provider.Multiscale.probeMeanGoodWaveConst_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) : 0 ≤ probeMeanGoodWaveConst M

theorem Algsuperdiff.Section3.Provider.Multiscale.probe_sum_collarLayer_meanSq_le_sqrt_mass_mul_sqrt_fourth {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (hstep : hn n ≤ hn (n + 1) + 1) (n1 n2 : ℤ) (omega : Cutoff.CutoffSample d) : ∑ Q ∈ collarLayer M m hn n omega, ∑ T ∈ Whitney.whitneySimplexCells m hn n Q, cellWeight m T * HCPolySupport.Book.Ch02.matrixOperatorNorm (simplexIncrementValue n1 n2 (↑omega) T) ^ 2 ≤ √(∑ Q ∈ collarLayer M m hn n omega, Whitney.cubeMassRatio (HCPolySupport.originCube d m) Q) * √(layerSimplexFourthMass m hn n n1 n2 omega)