move

RemyDegenne · Oct 17, 2024 · da37c22 · da37c22
1 parent 1efdf0f
commit da37c22
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 4 deletions.
diff --git a/TestingLowerBounds.lean b/TestingLowerBounds.lean
@@ -18,7 +18,7 @@ import TestingLowerBounds.Divergences.StatInfo.fDivStatInfo
 import TestingLowerBounds.Divergences.TotalVariation
 import TestingLowerBounds.ErealLLR
 import TestingLowerBounds.FDiv.Basic
-import TestingLowerBounds.FDiv.CompProd
+import TestingLowerBounds.FDiv.CompProd.CompProd
 import TestingLowerBounds.FDiv.CompProd.EqTopIff
 import TestingLowerBounds.FDiv.CondFDiv
 import TestingLowerBounds.FDiv.CondFDivCompProdMeasure

diff --git a/TestingLowerBounds/FDiv/CompProd.lean → ...ngLowerBounds/FDiv/CompProd/CompProd.lean b/TestingLowerBounds/FDiv/CompProd.lean → ...ngLowerBounds/FDiv/CompProd/CompProd.lean
diff --git a/TestingLowerBounds/FDiv/CondFDiv.lean b/TestingLowerBounds/FDiv/CondFDiv.lean
@@ -5,7 +5,7 @@ Authors: Rémy Degenne, Lorenzo Luccioli
 -/
 import Mathlib.MeasureTheory.Order.Group.Lattice
 import Mathlib.Probability.Kernel.Integral
-import TestingLowerBounds.FDiv.CompProd
+import TestingLowerBounds.FDiv.CompProd.CompProd
 import TestingLowerBounds.ForMathlib.CountableOrCountablyGenerated
 
 /-!

diff --git a/TestingLowerBounds/FDiv/DPIJensen.lean b/TestingLowerBounds/FDiv/DPIJensen.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import TestingLowerBounds.FDiv.CompProd
+import TestingLowerBounds.FDiv.CompProd.CompProd
 import TestingLowerBounds.FDiv.Trim
 import TestingLowerBounds.ForMathlib.RNDerivEqCondexp
 import TestingLowerBounds.Sorry.Jensen

diff --git a/TestingLowerBounds/ForMathlib/LogLikelihoodRatioCompProd.lean b/TestingLowerBounds/ForMathlib/LogLikelihoodRatioCompProd.lean
@@ -1,6 +1,6 @@
 import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
-import TestingLowerBounds.FDiv.CompProd
+import TestingLowerBounds.FDiv.CompProd.CompProd
 import TestingLowerBounds.FDiv.Measurable
 
 open Real MeasureTheory MeasurableSpace