ML.Causal­Application

This roll-up is the causal-application layer for Causalean.ML, kept separate from the causal-free core.

Regression­Bridge 3 core · 1 supporting This file is part of the causal-application layer of Causalean.ML: files under Causalean/ML/CausalApplication/ may import causal and estimation modules, while the Causalean/ML/ core remains causal-free. ★ isResidualOrthogonal_of_condExp★ condExp_of_isResidualOrthogonal

Conditional expectations as squared-loss population targets

This file is part of the causal-application layer of Causalean.ML: files under Causalean/ML/CausalApplication/ may import causal and estimation modules, while the Causalean/ML/ core remains causal-free.

The ML population-target keystone (square_loss_population_target_of_isResidualOrthogonal) is stated for a function whose residual is orthogonal to every function of the covariate (IsResidualOrthogonal). Here we connect that to Mathlib's condExp: the conditional mean E[Y ∣ X] is characterized by that moment condition under the stated integrability assumptions. With the additional finite-risk and cross-term assumptions in the population-target theorem, this condition can be used to establish squared-loss risk comparisons.

def covarSigma reviewed
Causalean.ML.CausalApplication

The covariate σ-algebra retains exactly covariate-observable events on a joint covariate--response sample, for a measurable covariate space.

Definition (Lean source)
parameters
X :
Type u_1
shared
def
covarSigma :
MeasurableSpace (X × ℝ)
given by
comap fst inferInstance
Causalean.ML.CausalApplication.covarSigma · Causalean/ML/CausalApplication/RegressionBridge.lean:36
theorem isResidualOrthogonal_of_condExp reviewed
Causalean.ML.CausalApplication

A conditional-mean candidate has residual orthogonal to every admissible covariate function under a finite joint covariate--response law on a measurable covariate space, provided the candidate is measurable, the response is integrable, and the candidate agrees almost everywhere with the response conditional mean given the covariate σ-algebra.

Formal statement
hypotheses
X :
Type u_1
shared
P :
Measure (X × ℝ)
IsFiniteMeasure P
m :
X → ℝ
hm :
Measurable m
hY :
Integrable (fun z => z.2) P
hcond :
(fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)])
conclusion
IsResidualOrthogonal P m
Proof (Lean source)
theorem isResidualOrthogonal_of_condExp (P : Measure (X × ℝ)) [IsFiniteMeasure P] {m : X → ℝ} (hm : Measurable m) (hY : Integrable (fun z => z.2) P) (hcond : (fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)])) : IsResidualOrthogonal P m := by intro g hgm hg have hF : covarSigma (X := X) ≤ (inferInstance : MeasurableSpace (X × ℝ)) := covarSigma_le (X := X) have hfst : Measurable[covarSigma (X := X)] (fun z : X × ℝ => z.1) := by rw [measurable_iff_comap_le] exact le_rfl have hM_sm : StronglyMeasurable[covarSigma (X := X)] (fun z : X × ℝ => m z.1) := by fun_prop have hG_sm : StronglyMeasurable[covarSigma (X := X)] (fun z : X × ℝ => g z.1) := by fun_prop have hM_int : Integrable (fun z : X × ℝ => m z.1) P := by exact (MeasureTheory.integrable_condExp (μ := P) (m := covarSigma (X := X)) (f := fun z : X × ℝ => z.2)).congr hcond.symm have hres_int : Integrable (fun z : X × ℝ => z.2 - m z.1) P := hY.sub hM_int have hM_ce : P[(fun z : X × ℝ => m z.1) | covarSigma (X := X)] = (fun z : X × ℝ => m z.1) := by exact MeasureTheory.condExp_of_stronglyMeasurable hF hM_sm hM_int have hres_ce : P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] =ᵐ[P] 0 := by calc P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] =ᵐ[P] P[(fun z : X × ℝ => z.2) | covarSigma (X := X)] - P[(fun z : X × ℝ => m z.1) | covarSigma (X := X)] := by condexp_linearity _ =ᵐ[P] P[(fun z : X × ℝ => z.2) | covarSigma (X := X)] - (fun z : X × ℝ => m z.1) := by rw [hM_ce] _ =ᵐ[P] 0 := by filter_upwards [hcond] with z hz change P[(fun z : X × ℝ => z.2) | covarSigma (X := X)] z - m z.1 = 0 rw [← hz] simp have hprod_ce : P[(fun z : X × ℝ => (z.2 - m z.1) * g z.1) | covarSigma (X := X)] =ᵐ[P] 0 := by calc P[(fun z : X × ℝ => (z.2 - m z.1) * g z.1) | covarSigma (X := X)] =ᵐ[P] P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] * (fun z : X × ℝ => g z.1) := MeasureTheory.condExp_mul_of_stronglyMeasurable_right (μ := P) (m := covarSigma (X := X)) (f := fun z : X × ℝ => z.2 - m z.1) (g := fun z : X × ℝ => g z.1) hG_sm hg hres_int _ =ᵐ[P] 0 := by filter_upwards [hres_ce] with z hz change P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] z * g z.1 = 0 rw [hz] simp calc ∫ z, (z.2 - m z.1) * g z.1 ∂P = ∫ z, (P[(fun z : X × ℝ => (z.2 - m z.1) * g z.1) | covarSigma (X := X)]) z ∂P := by exact (MeasureTheory.integral_condExp hF (μ := P) (f := fun z : X × ℝ => (z.2 - m z.1) * g z.1)).symm _ = ∫ z, (0 : ℝ) ∂P := by exact integral_congr_ae hprod_ce _ = 0 := by simp
Causalean.ML.CausalApplication.isResidualOrthogonal_of_condExp · Causalean/ML/CausalApplication/RegressionBridge.lean:45 · uses covarSigma , IsResidualOrthogonal
theorem condExp_of_isResidualOrthogonal reviewed
Causalean.ML.CausalApplication

A residual-orthogonal candidate agrees almost everywhere with the response conditional mean given covariates under a finite joint covariate--response law on a measurable covariate space, provided the candidate is measurable, the response is integrable, the candidate evaluated at covariates is integrable, and every admissible covariate function is orthogonal to its residual.

Formal statement
hypotheses
X :
Type u_1
shared
P :
Measure (X × ℝ)
IsFiniteMeasure P
m :
X → ℝ
hm :
Measurable m
hY :
Integrable (fun z => z.2) P
hmint :
Integrable (fun z => m z.1) P
hproj :
IsResidualOrthogonal P m
conclusion
(fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)])
Proof (Lean source)
theorem condExp_of_isResidualOrthogonal (P : Measure (X × ℝ)) [IsFiniteMeasure P] {m : X → ℝ} (hm : Measurable m) (hY : Integrable (fun z => z.2) P) (hmint : Integrable (fun z => m z.1) P) (hproj : IsResidualOrthogonal P m) : (fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)]) := by have hF : covarSigma (X := X) ≤ (inferInstance : MeasurableSpace (X × ℝ)) := covarSigma_le (X := X) haveI : IsFiniteMeasure (P.trim hF) := isFiniteMeasure_trim hF haveI : SigmaFinite (P.trim hF) := inferInstance have hfst : Measurable[covarSigma (X := X)] (fun z : X × ℝ => z.1) := by rw [measurable_iff_comap_le] exact le_rfl have hM_aesm : AEStronglyMeasurable[covarSigma (X := X)] (fun z : X × ℝ => m z.1) P := by exact (hm.comp hfst).stronglyMeasurable.aestronglyMeasurable refine MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq hF hY (fun _s _hs _hfin => hmint.integrableOn) ?_ hM_aesm intro s hs hfin have hs_ambient : MeasurableSet s := hF _ hs change MeasurableSet[comap fst inferInstance] s at hs obtain ⟨A, hA, hAeq⟩ := hs let g₀ : X → ℝ := indicator A (fun _ => (1 : ℝ)) have hg₀ : Measurable g₀ := by fun_prop have hres_int : Integrable (fun z : X × ℝ => z.2 - m z.1) P := hY.sub hmint have hprod_eq_indicator : (fun z : X × ℝ => (z.2 - m z.1) * g₀ z.1) = s.indicator (fun z : X × ℝ => z.2 - m z.1) := by funext z by_cases hz : z ∈ s · have hzA : z.1 ∈ A := by rw [← hAeq] at hz exact hz simp [g₀, Set.indicator_of_mem hz, Set.indicator_of_mem hzA] · have hzA : z.1 ∉ A := by intro hzA exact hz (by rw [← hAeq] exact hzA) simp [g₀, Set.indicator_of_notMem hz, Set.indicator_of_notMem hzA] have hg₀int : Integrable (fun z : X × ℝ => (z.2 - m z.1) * g₀ z.1) P := by simpa [hprod_eq_indicator] using hres_int.indicator hs_ambient have horth : ∫ z, (z.2 - m z.1) * g₀ z.1 ∂P = 0 := hproj g₀ hg₀ hg₀int have hres_set_zero : ∫ z in s, z.2 - m z.1 ∂P = 0 := by rw [← MeasureTheory.integral_indicator (μ := P) hs_ambient, ← hprod_eq_indicator] exact horth have hsubeq : ∫ z in s, z.2 ∂P - ∫ z in s, m z.1 ∂P = 0 := by rw [← MeasureTheory.integral_sub hY.integrableOn hmint.integrableOn] exact hres_set_zero exact (sub_eq_zero.mp hsubeq).symm
Causalean.ML.CausalApplication.condExp_of_isResidualOrthogonal · Causalean/ML/CausalApplication/RegressionBridge.lean:120 · uses covarSigma , IsResidualOrthogonal
1 supporting declaration (lemmas, instances)
Nuisance 3 core · 0 supporting Using the conditional-expectation bridge (RegressionBridge), this file gives generic aliases showing that a candidate satisfying IsResidualOrthogonal agrees almost everywhere with the conditional expectation of an arbitr ★ response_condExp_ae_eq_of_isResidualOrthogonal★ auxiliaryResponse_condExp_ae_eq_of_isResidualOrthogonal★ mlNuisanceVec

Conditional-mean candidates for causal nuisance workflows

Using the conditional-expectation bridge (RegressionBridge), this file gives generic aliases showing that a candidate satisfying IsResidualOrthogonal agrees almost everywhere with the conditional expectation of an arbitrary real response. These aliases acquire an outcome-regression or propensity interpretation only after the supplied law is separately shown to be an arm-specific outcome law or a covariate--treatment-indicator law. No concrete learner is shown here to satisfy IsResidualOrthogonal. mlNuisanceVec packages candidates into the Estimation.ATE.NuisanceVec expected by the AIPW moment.

theorem response_condExp_ae_eq_of_isResidualOrthogonal reviewed
Causalean.ML.CausalApplication

Generic conditional-mean identification. A measurable candidate equals almost everywhere the response conditional mean given covariates under a finite covariate--real-response law on the measurable covariate space, provided the response is integrable, the candidate evaluated at the covariates is integrable, and every admissible covariate function is orthogonal to the residual.

Formal statement
hypotheses
γ :
Type u_1
shared
Pd :
Measure (γ × ℝ)
IsFiniteMeasure Pd
m :
γ → ℝ
hm :
Measurable m
hY :
Integrable (fun z => z.2) Pd
hmint :
Integrable (fun z => m z.1) Pd
hproj :
IsResidualOrthogonal Pd m
conclusion
(fun z => m z.1) =ᵐ[Pd] (Pd[fun z => z.2 | covarSigma (X := γ)])
Proof (Lean source)
theorem response_condExp_ae_eq_of_isResidualOrthogonal (Pd : Measure (γ × ℝ)) [IsFiniteMeasure Pd] {m : γ → ℝ} (hm : Measurable m) (hY : Integrable (fun z => z.2) Pd) (hmint : Integrable (fun z => m z.1) Pd) (hproj : IsResidualOrthogonal Pd m) : (fun z => m z.1) =ᵐ[Pd] (Pd[fun z => z.2 | covarSigma (X := γ)]) := condExp_of_isResidualOrthogonal Pd hm hY hmint hproj
Causalean.ML.CausalApplication.response_condExp_ae_eq_of_isResidualOrthogonal · Causalean/ML/CausalApplication/Nuisance.lean:30 · uses covarSigma , IsResidualOrthogonal
theorem auxiliaryResponse_condExp_ae_eq_of_isResidualOrthogonal reviewed
Causalean.ML.CausalApplication

Generic auxiliary-response identification. A measurable candidate equals almost everywhere the auxiliary response conditional mean given covariates under a finite covariate--real-response law on the measurable covariate space, provided the response is integrable, the candidate evaluated at the covariates is integrable, and every admissible covariate function is orthogonal to the residual.

Formal statement
hypotheses
γ :
Type u_1
shared
Pe :
Measure (γ × ℝ)
IsFiniteMeasure Pe
e :
γ → ℝ
he :
Measurable e
hD :
Integrable (fun z => z.2) Pe
heint :
Integrable (fun z => e z.1) Pe
hproj :
IsResidualOrthogonal Pe e
conclusion
(fun z => e z.1) =ᵐ[Pe] (Pe[fun z => z.2 | covarSigma (X := γ)])
Proof (Lean source)
theorem auxiliaryResponse_condExp_ae_eq_of_isResidualOrthogonal (Pe : Measure (γ × ℝ)) [IsFiniteMeasure Pe] {e : γ → ℝ} (he : Measurable e) (hD : Integrable (fun z => z.2) Pe) (heint : Integrable (fun z => e z.1) Pe) (hproj : IsResidualOrthogonal Pe e) : (fun z => e z.1) =ᵐ[Pe] (Pe[fun z => z.2 | covarSigma (X := γ)]) := condExp_of_isResidualOrthogonal Pe he hD heint hproj
Causalean.ML.CausalApplication.auxiliaryResponse_condExp_ae_eq_of_isResidualOrthogonal · Causalean/ML/CausalApplication/Nuisance.lean:45 · uses covarSigma , IsResidualOrthogonal
def mlNuisanceVec reviewed
Causalean.ML.CausalApplication

The machine-learning nuisance vector packages supplied estimates for AIPW: it stores the treatment-indexed outcome regressions as its outcome component, the propensity function as its propensity component, the outcome measurability certificates in their evidence field, and the propensity measurability certificate in its evidence field, all on the measurable covariate space.

Definition (Lean source)
parameters
γ :
Type u_1
shared
μ_fn :
Bool → γ → ℝ
e_fn :
γ → ℝ
hμ :
∀ b, Measurable (μ_fn b)
he :
Measurable e_fn
def
mlNuisanceVec μ_fn e_fn hμ he :
NuisanceVec γ
given by
clause 1
μ_fn := μ_fn
clause 2
e_fn := e_fn
clause 3
μ_meas := hμ
clause 4
e_meas := he
Causalean.ML.CausalApplication.mlNuisanceVec · Causalean/ML/CausalApplication/Nuisance.lean:61 · uses NuisanceVec
AIPWExample 1 core · 0 supporting This file proves an equality-transport lemma: when supplied outcome-regression and propensity functions already agree almost everywhere with both true nuisances, their packaged NuisanceVec makes the AIPW estimating equat ★ aipw_mlNuisance_meanZero_transport_of_exact_nuisances

Exact-nuisance transport into the AIPW mean-zero equation

This file proves an equality-transport lemma: when supplied outcome-regression and propensity functions already agree almost everywhere with both true nuisances, their packaged NuisanceVec makes the AIPW estimating equation mean-zero at the average treatment effect. No learner, empirical-risk minimizer, or convergence-rate hypothesis appears here, and the result does not state the one-nuisance-correct double-robust property. It reuses the existing exact-nuisance AIPW identification theorem.

theorem aipw_mlNuisance_meanZero_transport_of_exact_nuisances reviewed
Causalean.ML.CausalApplication

AIPW mean-zero transport under two exact nuisance equalities. In a backdoor estimation system, suppose the propensity is bounded away from 0 and 1 by ε (strict overlap), the backdoor identification assumptions hold, the squared factual outcome is integrable, and the squared potential outcome under each treatment arm is integrable. If the supplied outcome-regression functions and propensity function are measurable and agree almost everywhere under the covariate law with the true outcome regression and true propensity, respectively (correct specification), then the AIPW moment functional built from the supplied nuisance vector integrates to zero at the true average treatment effect S.θ₀. This lemma assumes both nuisance equalities; it does not expose the one-nuisance-correct double-robust guarantee or establish that a learner supplies either equality.

Formal statement
hypotheses
P :
POSystem
shared
γ :
Type u_1
shared
S :
BackdoorEstimationSystem P γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPOBackdoorSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
mhat :
Bool → γ → ℝ
ehat :
γ → ℝ
hmhat :
∀ b, Measurable (mhat b)
hehat :
Measurable ehat
hμ_spec :
∀ b, mhat b =ᵐ[S.P_X] S.μ_val b
he_spec :
ehat =ᵐ[S.P_X] S.e_val
conclusion
(∫ z, BackdoorEstimationSystem.aipwMomentFunctional (mlNuisanceVec mhat ehat hmhat hehat) z S.θ₀ ∂ S.P_Z)
= 0
Proof (Lean source)
theorem aipw_mlNuisance_meanZero_transport_of_exact_nuisances (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) {mhat : Bool → γ → ℝ} {ehat : γ → ℝ} (hmhat : ∀ b, Measurable (mhat b)) (hehat : Measurable ehat) (hμ_spec : ∀ b, mhat b =ᵐ[S.P_X] S.μ_val b) (he_spec : ehat =ᵐ[S.P_X] S.e_val) : (∫ z, BackdoorEstimationSystem.aipwMomentFunctional (mlNuisanceVec mhat ehat hmhat hehat) z S.θ₀ ∂ S.P_Z) = 0 := by have hproj : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) have hμZ (b : Bool) : (fun z => mhat b (projX z)) =ᵐ[S.P_Z] fun z => S.μ_val b (projX z) := by have hx := hμ_spec b rw [← BackdoorEstimationSystem.P_Z_map_projX_eq_P_X S] at hx exact (ae_map_iff hproj.aemeasurable (measurableSet_eq_fun (hmhat b) (S.μ_meas b))).mp hx have heZ : (fun z => ehat (projX z)) =ᵐ[S.P_Z] fun z => S.e_val (projX z) := by have hx := he_spec rw [← BackdoorEstimationSystem.P_Z_map_projX_eq_P_X S] at hx exact (ae_map_iff hproj.aemeasurable (measurableSet_eq_fun hehat S.e_meas)).mp hx have hfun : (fun z => BackdoorEstimationSystem.aipwMomentFunctional (mlNuisanceVec mhat ehat hmhat hehat) z S.θ₀) =ᵐ[S.P_Z] S.ψ_AIPW := by filter_upwards [hμZ true, hμZ false, heZ] with z hμ1 hμ0 he change aipwMoment z mhat ehat S.θ₀ = aipwMoment z S.μ_val S.e_val S.θ₀ unfold aipwMoment rw [hμ1, hμ0, he] rw [integral_congr_ae hfun] exact BackdoorEstimationSystem.aipw_mean_zero_of_square_integrable S h_overlap hA h_y2 h_yd2
Causalean.ML.CausalApplication.aipw_mlNuisance_meanZero_transport_of_exact_nuisances · Causalean/ML/CausalApplication/AIPWExample.lean:31 · uses BackdoorEstimationSystem , P_X , P_Z , StrictOverlap , aipwMomentFunctional , θ₀ , mlNuisanceVec , Assumptions , YofD , factualY , POSystem
Rate­Assembly 1 core · 1 supporting This file consumes abstract error sequences already assumed to have o_p(n^{-1/4}) rates and derives the three corresponding nuisance-rate conditions used by DML. ★ dml_rate_conditions_of_quarter_rates

Abstract quarter-rate assembly for DML nuisance conditions

This file consumes abstract error sequences already assumed to have o_p(n^{-1/4}) rates and derives the three corresponding nuisance-rate conditions used by DML. It does not connect those sequences to a concrete learner or invoke a method-specific AchievesL2Rate theorem.

It is method-agnostic: once a learner proves an o_p(n^{-1/4}) L²-rate toward a target that a separate identification argument equates almost everywhere with the causal nuisance, plug its error sequence in as μErr / eErr. Fixed-penalty ridge and logistic rates target penalized pseudo-true predictors; they do not by themselves provide this identification. Instantiating μErr a n ω := (eLpNorm (fun x => μ̂ n ω a x − μ_val a x) 2 P_X).toReal (and eErr analogously) makes the three outputs literally DML's h_mu_rate / h_e_rate / h_product_rate.

theorem dml_rate_conditions_of_quarter_rates reviewed
Causalean.ML.CausalApplication

Assembly. On a measurable sample space with sampling law, for outcome and propensity error sequences, if, for every treatment arm, the outcome-regression estimation error is o_p(n^{-1/4}), and the propensity estimation error is o_p(n^{-1/4}), then each error is separately o_p(1), and for every arm the pointwise product of the outcome and propensity errors is o_p(n^{-1/2}) — together these are DML's three nuisance-rate conditions.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Bool → ℕ → Ω → ℝ
ℕ → Ω → ℝ
shared
hμ :
∀ a, IsLittleOp (μErr a) (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ
he :
IsLittleOp eErr (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ
conclusion
conclusion 1
a :
IsLittleOp (μErr a) (fun _ => 1) μ
conclusion 2
IsLittleOp eErr (fun _ => 1) μ
conclusion 3
a :
IsLittleOp (fun n ω => μErr a n ω * eErr n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
Proof (Lean source)
theorem dml_rate_conditions_of_quarter_rates {μErr : Bool → ℕ → Ω → ℝ} {eErr : ℕ → Ω → ℝ} (hμ : ∀ a, IsLittleOp (μErr a) (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) (he : IsLittleOp eErr (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) : (∀ a, IsLittleOp (μErr a) (fun _ => 1) μ) ∧ IsLittleOp eErr (fun _ => 1) μ ∧ (∀ a, IsLittleOp (fun n ω => μErr a n ω * eErr n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) := ⟨fun a => isLittleOp_one_of_le_one rpow_quarter_le_one (hμ a), isLittleOp_one_of_le_one rpow_quarter_le_one he, fun a => isLittleOp_mul_quarter (hμ a) he⟩
Causalean.ML.CausalApplication.dml_rate_conditions_of_quarter_rates · Causalean/ML/CausalApplication/RateAssembly.lean:44 · uses IsLittleOp
1 supporting declaration (lemmas, instances)
  • rpow_quarter_le_one theorem — For a sample size, the n^{-1/4} rate is bounded by 1, so it weakens to the o_p(1) rate.
    hypotheses
    n :
    ℕ
    conclusion
    (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ 1
    Proof (Lean source)
    theorem rpow_quarter_le_one (n : ℕ) : (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ 1 := by rcases Nat.eq_zero_or_pos n with hn | hn · subst hn simp · have h1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn exact Real.rpow_le_one_of_one_le_of_nonpos h1 (by norm_num)
    Causalean.ML.CausalApplication.rpow_quarter_le_one · Causalean/ML/CausalApplication/RateAssembly.lean:35