Guarded continuous Dudley capstone on the unit interval

This module instantiates the guarded positive-radius continuous Dudley passage on the concrete unit-interval Rademacher linear process. The entropy profile is real-valued, nonconstant, and used only through dyadic guarded annuli, avoiding the old global Antitone (ℝ → ℝ) continuous theorem surface.

def FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalRoundedGridCoverProfile (j : ℕ) : ℕ

Dyadic-indexed rounded-grid cover-count profile for the unit interval.

Equations

• FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalRoundedGridCoverProfile j = FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridCoverCount j

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitInterval_coverProfile_eq_roundedDyadicGridCoverCount (j : ℕ) : unitIntervalRoundedGridCoverProfile j = UnitIntervalDudley.unitIntervalRoundedDyadicGridCoverCount j

The dyadic-indexed profile is definitionally the rounded-grid cover count.

This is intentionally a dyadic-indexed statement, not a global real-radius covering-number antitonicity claim.

noncomputable def FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalEntropyProfile (ε : ℝ) : ℝ

A bounded, nonconstant positive entropy profile used for the guarded unit-interval capstone.

Equations

• FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalEntropyProfile ε = 20 + Real.exp (-ε)

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalEntropyProfile_nonneg (ε : ℝ) : 0 ≤ unitIntervalEntropyProfile ε

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalEntropyProfile_antitone : Antitone unitIntervalEntropyProfile

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalEntropyProfile_guarded (j : ℕ) : GuardedDudleyIntegral.GuardedAntitoneOnDyadicAnnulus unitIntervalEntropyProfile 1 j

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalEntropyProfile_intervalIntegrable (a b : ℝ) : IntervalIntegrable unitIntervalEntropyProfile MeasureTheory.volume a b

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitInterval_entropyProfile_nonconstant : unitIntervalEntropyProfile 0 ≠ unitIntervalEntropyProfile 1

The entropy integrand is load-bearing: it is not a constant profile.

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitInterval_entropyProfile_integral_positive : 0 < ∫ (ε : ℝ) in 0..1 / 2, unitIntervalEntropyProfile ε

The entropy integrand has positive mass on the continuous Dudley interval.

noncomputable def FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalDivergingEntropyProfile (ε : ℝ) : ℝ

Positive-radius singular entropy profile. It is zero off positive radii, but diverges like ε^(-1/2) as ε ↓ 0 along positive radii.

Equations

• FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalDivergingEntropyProfile ε = if 0 < ε then 20 * ε ^ (-1 / 2) else 0

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalDivergingEntropyProfile_nonneg (ε : ℝ) : 0 ≤ unitIntervalDivergingEntropyProfile ε

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalDivergingEntropyProfile_guarded (j : ℕ) : GuardedDudleyIntegral.GuardedAntitoneOnDyadicAnnulus unitIntervalDivergingEntropyProfile 1 j

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalDivergingEntropyProfile_intervalIntegrable_zero_half : IntervalIntegrable unitIntervalDivergingEntropyProfile MeasureTheory.volume 0 (1 / 2)

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitIntervalDivergingEntropyProfile_intervalIntegrable_dyadic (j : ℕ) : IntervalIntegrable unitIntervalDivergingEntropyProfile MeasureTheory.volume (1 / 2 ^ (j + 2)) (1 / 2 ^ (j + 1))

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitInterval_divergingEntropyProfile_dominates_roundedDyadicEntropy (j : ℕ) : √(Real.log ↑(UnitIntervalDudley.unitIntervalRoundedDyadicGridCoverCount j)) ≤ unitIntervalDivergingEntropyProfile (1 / 2 ^ (j + 1))

The singular profile dominates every rounded-dyadic entropy sample.

-- fidelity: The domination is uniform in the dyadic index and uses the actual rounded-grid cover counts, while the profile diverges at positive radii approaching zero.

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.unitInterval_divergingEntropyProfile_integral_positive : 0 < ∫ (ε : ℝ) in 0..1 / 2, unitIntervalDivergingEntropyProfile ε

The singular entropy profile has positive integral mass on 0..1/2.

-- fidelity: The positive lower bound comes from the concrete subinterval [1 / 4, 1 / 2], so the load-bearing entropy term is not concentrated in a formal singularity at zero.

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.continuous_dudley_entropy_integral_iSup_of_dyadicProfile_guarded {Ω : Type u_1} {T : Type u_2} [Fintype Ω] (P : FiniteSubGaussianChaining.FiniteSubGaussianProcess Ω T) (coarseBudget radiusScale : ℝ) (entropyAtRadius : ℝ → ℝ) (supFunctional : Ω → ℝ) (hradiusScale : 0 < radiusScale) (hentropy_nonneg : ∀ (ε : ℝ), 0 ≤ entropyAtRadius ε) (hint0 : IntervalIntegrable entropyAtRadius MeasureTheory.volume 0 (radiusScale / 2)) (hdyadic : ∀ (eta : ℝ), 0 < eta → ∃ (m : ℕ), (∀ j ∈ Finset.range m, GuardedDudleyIntegral.GuardedAntitoneOnDyadicAnnulus entropyAtRadius radiusScale j) ∧ (∀ j ∈ Finset.range m, IntervalIntegrable entropyAtRadius MeasureTheory.volume (radiusScale / 2 ^ (j + 2)) (radiusScale / 2 ^ (j + 1))) ∧ FiniteSubGaussianChaining.finiteExpectation P.weight supFunctional ≤ coarseBudget + 2 * √(2 * P.varianceProxy) * FiniteSubGaussianChaining.FiniteSubGaussianProcess.finiteDyadicEntropyAtRadiusUpperSum radiusScale m entropyAtRadius + eta) : FiniteSubGaussianChaining.finiteExpectation P.weight supFunctional ≤ coarseBudget + 4 * √(2 * P.varianceProxy) * ∫ (ε : ℝ) in 0..radiusScale / 2, entropyAtRadius ε

Corrected guarded continuous Dudley wrapper using a dyadic profile side condition instead of a global antitone entropy profile.

-- fidelity: The finite input is a real dyadic upper-sum bound at positive annuli; the theorem does not assume global antitonicity or evaluate the profile at radius zero through monotonicity.

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.continuous_dudley_entropy_integral_iSup_unitInterval : FiniteSubGaussianChaining.finiteExpectation UnitIntervalDudley.unitIntervalRademacherLinearProcess.weight UnitIntervalDudley.unitIntervalRademacherLinearSup ≤ 1 + 4 * √(2 * UnitIntervalDudley.unitIntervalRademacherLinearProcess.varianceProxy) * ∫ (ε : ℝ) in 0..1 / 2, unitIntervalEntropyProfile ε

Continuous Dudley entropy-integral bound for the nonzero unit-interval Rademacher linear process with a nonconstant entropy integrand.

-- fidelity: The process is the concrete nonzero sign * t process on the non-finite unit interval, the supremum functional has expectation 1 / 2, and the entropy profile is separately proved nonconstant with positive integral.

theorem FormalSLT.Covering.ContinuousDudleyUnitInterval.continuous_dudley_entropy_integral_iSup_unitInterval_diverging : FiniteSubGaussianChaining.finiteExpectation UnitIntervalDudley.unitIntervalRademacherLinearProcess.weight UnitIntervalDudley.unitIntervalRademacherLinearSup ≤ 1 + 4 * √(2 * UnitIntervalDudley.unitIntervalRademacherLinearProcess.varianceProxy) * ∫ (ε : ℝ) in 0..1 / 2, unitIntervalDivergingEntropyProfile ε

Continuous Dudley entropy-integral bound for the unit-interval process using the integrable positive-radius singular entropy profile.

-- fidelity: This capstone uses the same concrete nonzero process and supplied supremum as the bounded-profile theorem, but its entropy profile diverges as ε ↓ 0 along positive radii and dominates every rounded-dyadic entropy sample.